1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), FSCD 2016, June 22-26, 2016, Porto, Portugal
FSCD 2016
June 22-26, 2016
Porto, Portugal
Formal Structures for Computation and Deduction
FSCD
https://fscd-conference.org/
https://dblp.org/db/conf/fscd
Leibniz International Proceedings in Informatics
LIPIcs
https://www.dagstuhl.de/dagpub/1868-8969
https://dblp.org/db/series/lipics
1868-8969
Delia
Kesner
Delia Kesner
Brigitte
Pientka
Brigitte Pientka
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
52
2016
978-3-95977-010-1
https://www.dagstuhl.de/dagpub/978-3-95977-010-1
Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee
Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee
Front Matter
Table of Contents
Preface
Steering Committee
Program Committee
External Reviewers
Organising Commitee
0:i-0:xviii
Front Matter
Delia
Kesner
Delia Kesner
Brigitte
Pientka
Brigitte Pientka
10.4230/LIPIcs.FSCD.2016.0
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Compositional Compiler Verification for a Multi-Language World
Verified compilers are typically proved correct under severe
restrictions on what the compiler's output may be linked with, from no
linking at all to linking only with code compiled from the same source
language. Such assumptions contradict the reality of how we use these
compilers since most software systems today are comprised of
components written in different languages compiled by different
compilers to a common target, as well as low-level libraries that may
be handwritten in the target language.
The key challenge in verifying compilers for today's world of
multi-language software is how to formally state a compiler
correctness theorem that is compositional along two dimensions.
First, the theorem must guarantee correct compilation of components
while allowing compiled code to be composed (linked) with
target-language components of arbitrary provenance, including those
compiled from other languages. Second, the theorem must support
verification of multi-pass compilers by composing correctness proofs
for individual passes. In this talk, I will describe a methodology
for verifying compositional compiler correctness for a higher-order
typed language and discuss the challenges that lie ahead. I will
argue that compositional compiler correctness is, in essence, a
language interoperability problem: for viable solutions in the long
term, high-level languages must be equipped with principled
foreign-function interfaces that specify safe interoperability
between high-level and low-level components, and between more
precisely and less precisely typed code.
verified compilation; compositional compiler correctness
multi-language semantics
typed low-level languages
1:1-1:1
Regular Paper
Amal
Ahmed
Amal Ahmed
10.4230/LIPIcs.FSCD.2016.1
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Coalgebras and Higher-Order Computation: a GoI Approach
Girard's geometry of interaction (GoI) can be seen---in one practical
aspect of it---as a compositional compilation method from functional
programs to sequential machines. There tokens move around and express
interactions between (parts of) programs. Intrigued by the combination
of abstract structures and concrete dynamics in GoI, our line of work
has aimed at exploiting, in GoI, results from the theory of
coalgebra---a categorical abstraction of state-based transition
systems that has found its use principally in concurrency theory. Such
reinforced connection between higher-order computation and state-based
dynamics is made possible thanks to an elegant categorical
axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced
monoidal categories are identified to be the essential structure
behind. In the talk I shall lay out these basic ideas, together with
some of our results on: GoI semantics for a quantum programming
language; and our ``memoryful'' extension of GoI with algebraic
effects.
The talk is based on my joint work with my colleague Naohiko Hoshino (RIMS, Kyoto Univer- sity) and my (former) students Koko Muroya (University of Birmingham) and Toshiki Kataoka
(University of Tokyo), to whom I owe special thanks.
functional programming
geometry of interaction
categorical semantics
coalgebra
2:1-2:2
Regular Paper
Ichiro
Hasuo
Ichiro Hasuo
10.4230/LIPIcs.FSCD.2016.2
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization
We describe experiments in teaching fundamental informatics notions around mathematical structures for formal concepts, and effective algorithms to manipulate them. The major themes of lambda-calculus and type theory served as guides for the effective implementation of functional programming languages and higher-order proof assistants, appropriate for reflecting the theoretical material into effective tools to represent constructively the concepts and formally certify the proofs of their properties. Progressively, a literate programming and proving style replaced informal mathematics in the presentation of the material as executable course notes. The talk will evoke the various stages of (in)completion of the corresponding set of notes along the years, and tell how their elaboration proved to be essential to the discovery of fundamental results.
Foundations
Computation
Deduction
Programming
Proofs
3:1-3:2
Regular Paper
Gérard
Huet
Gérard Huet
10.4230/LIPIcs.FSCD.2016.3
Gérard Huet. Initiation à la logique mathématique. Notes de cours du DEA d'Informatique, Université Paris-Sud, 1977.
Gérard Huet. Démonstration automatique en logique de premier ordre et programmation en clauses de horn. Notes de cours du DEA d'Informatique, Université Paris-Sud, 1978.
Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27,4:797-821, 1980.
Gérard Huet. Deduction and computation. In Manfred Broy, editor, Logic of Programming and Calculi of Discrete Design, pages 305-342. Springer Verlag, 1987.
Gérard Huet. Initiation au λ-calcul. Notes de cours du DEA "Fonctionalité, Structures de Calcul et Programmation, Université Paris VII, 1987.
Gérard Huet. Introduction au λ-calcul pur. In Friedrich Bauer, editor, Logic, Algebra and Computation, pages 153-200. Springer Verlag, 1987.
Gérard Huet. Induction principles formalized in the calculus of constructions. In K. Fuchi and M. Nivat, editors, Programming of Future Generation Computers, pages 205-216. North Holland, 1988.
Gérard Huet. Cartesian closed categories and lambda-calculus. In Gérard Huet, editor, Logical Foundations of Functional Programming, pages 7-23. Addison-Wesley, 1989.
Gérard Huet. The Constructive Engine. In R. Narasimhan, editor, A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney. World Scientific Publishing, 1989.
Gérard Huet. A uniform approach to type theory. In Gérard Huet, editor, Logical Foundations of Functional Programming, pages 337-397. Addison-Wesley, 1989.
Gérard Huet. An analysis of Böhm’s theorem. Theoretical Computer Science, 121:145-167, 1993.
Gérard Huet. Constructive computation theory. Course Notes, DEA Informatique, Mathématiques et Applications, Paris VII, 1987, 1993. URL: http://yquem.inria.fr/~huet/PUBLIC/CCT.pdf.
http://yquem.inria.fr/~huet/PUBLIC/CCT.pdf
Gérard Huet. Residual theory in λ-calculus: a formal development. J. Functional Programming, 4,3:371-394, 1994.
Gérard Huet. Initiation à la théorie des catégories. Notes de cours du DEA "Fonctionalité, Structures de Calcul et Programmation, Université Paris VII, 2nd edition, 1987.
Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. of Computer and System Sciences, 23,1:11-21, I981.
Gérard Huet. Formal structures for computation and deduction. Course Notes, Carnegie-Mellon University, May 1986. URL: http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.pdf.
http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.pdf
Gérard Huet and Derek Oppen. Equations and rewrite rules: a survey. In Ronald Book, editor, Formal Languages: Perspectives and Open Problems, pages 349-405. Academic Press, 1980.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Verified Analysis of Functional Data Structures
In recent work the author has analyzed a number of classical
functional search tree and priority queue implementations with the
help of the theorem prover Isabelle/HOL. The functional correctness
proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2
brother trees, AA trees and splay trees could be automated. The
amortized logarithmic complexity of skew heaps, splay trees, splay
heaps and pairing heaps had to be proved manually.
Program Verification
Algorithm Analysis
Functional Programming
4:1-4:2
Regular Paper
Tobias
Nipkow
Tobias Nipkow
10.4230/LIPIcs.FSCD.2016.4
Martin Avanzini, Georg Moser, and Michael Schaper. TcT: Tyrolean Complexity Tool. In M. Chechik and J.-F. Raskin, editors, TACAS, volume 9636 of LNCS, pages 407-423. Springer, 2016.
Hauke Brinkop. Verifikation der amortisierten Laufzeit von Pairing Heaps in Isabelle. Bachelor’s thesis, Fakultät für Informatik, Technische Universität München, 2015.
Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In C. Urban and X. Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 137-153. Springer, 2015.
Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14, 2012.
Tobias Nipkow. Amortized complexity verified. Archive of Formal Proofs, 2014. http://isa-afp.org/entries/Amortized_Complexity.shtml, Formal proof development.
http://isa-afp.org/entries/Amortized_Complexity.shtml
Tobias Nipkow. Amortized complexity verified. In C. Urban and X. Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 310-324. Springer, 2015.
Tobias Nipkow. Automatic functional correctness proofs for functional search trees. In J. Blanchette and S. Merz, editors, ITP 2016, LNCS. Springer, 2015. To appear.
Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
http://concrete-semantics.org
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
Lars Noschinski, Fabian Emmes, and Jürgen Giesl. Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reasoning, 51(1):27-56, 2013.
Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter P. Puschner, Jan Staschulat, and Per Stenström. The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst., 7(3), 2008.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.
Following Aehlig, we consider a hierarchy F^p= { F^p_n }_{n in Nat} of
parameter-free subsystems of System F, where each F^p_n
corresponds to ID_n, the theory of n-times iterated inductive
definitions (thus our F^p_n corresponds to the n+1th system of
Aehlig). We here present two proofs of strong normalization for
F^p_n, which are directly formalizable with inductive definitions.
The first one, based on the Joachimski-Matthes method, can be fully
formalized in ID_n+1. This provides a tight upper bound on the
complexity of the normalization theorem for System F^p_n. The
second one, based on the Godel-Tait method, can be locally
formalized in ID_n. This provides a direct proof to the known
result that the representable functions in F^p_n are provably
total in ID_n. In both cases, Buchholz' Omega-rule plays a
central role.
Polymorphic Lambda Calculus
Strong Normalization
Computability Predicate
Infinitary Proof Theory
5:1-5:15
Regular Paper
Ryota
Akiyoshi
Ryota Akiyoshi
Kazushige
Terui
Kazushige Terui
10.4230/LIPIcs.FSCD.2016.5
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Normalisation by Evaluation for Dependent Types
We develop normalisation by evaluation (NBE) for dependent types based
on presheaf categories. Our construction is formulated using internal
type theory using quotient inductive types. We use a typed
presentation hence there are no preterms or realizers in our
construction. NBE for simple types is using a logical relation between
the syntax and the presheaf interpretation. In our construction, we
merge the presheaf interpretation and the logical relation into a
proof-relevant logical predicate. We have formalized parts of the
construction in Agda.
normalisation by evaluation
dependent types
internal type theory
logical relations
Agda
6:1-6:16
Regular Paper
Thorsten
Altenkirch
Thorsten Altenkirch
Ambrus
Kaposi
Ambrus Kaposi
10.4230/LIPIcs.FSCD.2016.6
Andreas Abel. Towards normalization by evaluation for the βη-calculus of constructions. In Functional and Logic Programming, pages 224-239. Springer, 2010.
Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. PhD thesis, Habilitation, Ludwig-Maximilians-Universität München, 2013.
Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium on, pages 3-12. IEEE, 2007.
The Agda Wiki, 2015. Available online.
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Phil Scott. Normalization by evaluation for typed lambda calculus with coproducts. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 303-310, 2001.
Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David Pitt, David E. Rydeheard, and Peter Johnstone, editors, Category Theory and Computer Science, LNCS 953, pages 182-199, 1995.
Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for a polymorphic system. In 11th Annual IEEE Symposium on Logic in Computer Science, pages 98-106, 1996.
Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for system F. Manuscript, 1997. URL: http://www.cs.nott.ac.uk/~txa/publ/f97.pdf.
http://www.cs.nott.ac.uk/~txa/publ/f97.pdf
Thorsten Altenkirch and Ambrus Kaposi. Agda formalisation for the paper Normalisation by Evaluation for Dependent Types, 2016. Available online at the second author’s website.
Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 18-29, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2837614.2837638.
http://dx.doi.org/10.1145/2837614.2837638
Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Logic in Computer Science, 1991. LICS'91., Proceedings of Sixth Annual IEEE Symposium on, pages 203-211. IEEE, 1991.
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Manuscript, December 2015.
Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Types for Proofs and Programs, pages 93-109. Springer, 2006.
Olivier Danvy. Type-directed partial evaluation. Springer, 1999.
Peter Dybjer. Internal type theory. In Types for Proofs and Programs, pages 120-134. Springer, 1996.
Martin Hofmann. Syntax and semantics of dependent types. In Extensional Constructs in Intensional Type Theory, pages 13-54. Springer, 1997.
Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de Bruijn substitution algebra in Coq. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 67-73. ACM, 2015.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency
Paradefinite (`beyond the definite') logics are logics that can be
used for handling contradictory or partial information. As such,
paradefinite logics should be both paraconsistent and paracomplete. In
this paper we consider the simplest semantic framework for defining
paradefinite logics, consisting of four-valued matrices, and study the
better accepted logics that are induced by these matrices.
Paraconsistecy
Paracompleteness
4-valued logics
7:1-7:15
Regular Paper
Ofer
Arieli
Ofer Arieli
Arnon
Avron
Arnon Avron
10.4230/LIPIcs.FSCD.2016.7
O. Arieli. Paraconsistent reasoning and preferential entailments by signed quantified Boolean formulae. ACM Transactions on Computational Logic, 8(3), 2007.
O. Arieli and A. Avron. The value of the four values. Artificial Intelligence, 102(1):97-141, 1998.
O. Arieli, A. Avron, and A. Zamansky. Ideal paraconsistent logics. Studia Logica, 99(1-3):31-60, 2011.
O. Arieli and M. Denecker. Reducing preferential paraconsistent reasoning to classical entailment. Logic and Computation, 13(4):557-580, 2003.
A. Avron. Simple consequence relations. Information and Computation, 92(1):105-140, 1991.
A. Avron. On the expressive power of three-valued and four-valued languages. Journal of Logic and Computation, 9(6):977-994, 1999.
A. Avron, J. Ben-Naim, and B. Konikowska. Processing information from a set of sources. In Towards Mathematical Philosophy, Trends in Logic, volume 10, pages 165-186. Springer, 2009.
A. Avron and B. Konikowska. Multi-valued calculi for logics based on non-determinism. Logic Journal of the IGPL, 13(4):365-387, 2005.
N. Belnap. How a computer should think. In G. Ryle, editor, Contemporary Aspects of Philosophy, pages 30-56. Oriel Press, 1977.
N. Belnap. A useful four-valued logic. In J. M. Dunn and G. Epstein, editors, Modern Uses of Multiple-Valued Logics, pages 7-37. Reidel Publishing Company, 1977.
J. Y. Béziau. Bivalent semantics for De Morgan logic (The uselessness of four-valuedness). In W. A. Carnielli, M. E. Coniglio, and I. M. L. D'Ottaviano, editors, The many sides of logic, pages 391-402. College Publication, 2009.
F. Bou and U. Rivieccio. The logic of distributive bilattices. Logic Journal of the IGPL, 19(1):183-216, 2010.
N. da Costa. On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic, 15:497-510, 1974.
J. M. Dunn. The Algebra of Intensional Logics. PhD thesis, University of Pittsburgh, Ann Arbor (UMI), 1966.
J. M. Dunn. Intuitive semantics for first-degree entailments and coupled trees. Philosophical Studies, 29:149-168, 1976.
M. Fitting. Bilattices and the semantics of logic programming. Journal of Logic Programming, 11(2):91-116, 1991.
M. Fitting. The family of stable models. Journal of Logic Programming, 17:197-225, 1993.
G. Gentzen. Investigations into logical deduction, 1934. In German. An English translation appears in `The Collected Works of Gerhard Gentzen', edited by M. E. Szabo, North-Holland, 1969.
S. Gottwald. A treatise on many-valued logics. In Studies in Logic and Computation, volume 9. Research Studies Press, Baldock, 2001.
G. Malinowski. Many-Valued Logics. Clarendon Press, 1993.
D. J. Shoesmith and T. J. Smiley. Deducibility and many-valuedness. Journal of Symbolic Logic, 36:610-622, 1971.
D. J. Shoesmith and T. J. Smiley. Multiple Conclusion Logic. Cambridge University Press, 1978.
G. Takeuti. Proof Theory. Elsevier, 1975.
A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2000.
A. Urquhart. Many-valued logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, pages 249-295. Kluwer, 2001. Second edition.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus
Development of a contraction-free BI sequent calculus, be the
contraction-freeness implicit or explicit, has not been successful in
the literature. We address this problem by presenting such a sequent
system. Our calculus involves no structural rules. It should be an
insight into non-formula contraction absorption in other non-classical
logics. Contraction absorption in sequent calculus is associated to
simpler cut elimination and to efficient proof searches.
cut-elimination
contraction-free
sequent calculus
proof theory
BI
logic combination
8:1-8:18
Regular Paper
Ryuta
Arisaka
Ryuta Arisaka
10.4230/LIPIcs.FSCD.2016.8
Ryuta Arisaka, Anupam Das, and Lutz Straßburger. On Nested Sequents for Constructive Modal Logics. Logical Methods in Computer Science, 11(3), 2015.
Ryuta Arisaka and Shengchao Qin. LBI cut elimination proof with BI-Multi-Cut. In TASE, pages 235-238, 2012.
Nuel Belnap. Display logic. Journal of Philosophical Logic, 11(4):375-417, 1982.
James Brotherston and Cristiano Calcagno. Classical BI: a logic for reasoning about dualising resources. In POPL, pages 328-339, 2009.
Carlos Caleiro and Jaime Ramos. Combining classical and intuitionistic implications. In Frontiers of Combining Systms, pages 118-132, 2007.
Luis Fariñas del Cerro and Andreas Herzig. Combining classical and intuitionistic logic, or: Intuitionistic implication as a conditional. In Frontiers of Combining Systms, pages 93-102, 1996.
Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, and Sungwoo Park. The inverse method for the logic of bunched implications. In LPAR, pages 466-480, 2004.
Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log., 57(3):795-807, 1992.
Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and resource tableaux. Mathematical Structures in Computer Science, 15(6):1033-1088, 2005. URL: http://dx.doi.org/10.1017/S0960129505004858.
http://dx.doi.org/10.1017/S0960129505004858
Steve Giambrone. TW_+ AND RW_+ ARE DECIDABLE. Journal of Philosophical Logic, 14(3):235-254, 1985.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987.
Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof search for bi-intuitionistic tense logic. CoRR, abs/1006.4793, 2010.
Haskell B. Curry. A Theory of Formal Deductibility. University of Notre Dame, 1950.
Norihiro Kamide. Temporal BI: Proof system, semantics and translations. Theor. Comput. Sci., 492:40-69, 2013.
Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-135, 1994.
Stephen C. Kleene. Introduction to META-MATHEMATICS. North-Holland Publishing Co., 1952.
Sonia Marin and Lutz Straßburger. Label-free Modular Systems for Classical and Intuitionistic Modal Logics. In Advances in Modal Logic, pages 387-406, 2014.
Robert K. Meyer and Michael A. McRobbie. Multisets and relevant implication I. Australasian Journal of Philosophy, 60(3):107-139, 1982.
Robert K. Meyer and Michael A. McRobbie. Multisets and relevant implication II. Australasian Journal of Philosophy, 60(3):265-281, 1982.
Michael Moortgat. Categorial type logics. HANDBOOK OF LOGIC AND LANGUAGE, pages 93-177, 1997.
Peter W. O'Hearn. On bunched typing. Journal of Functional Programming, 13(4):747-796, 2003.
Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999.
Dag Prawitz. Natural Deduction - A Proof-Theoretical Study. Almquist and Wiksell, 1965.
David J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, 2002.
Anne S. Troelstra and Helmut Schwichtenberg. Basic proof theory (2nd ed.). Cambridge University Press, 2000.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
We present sound and complete environmental bisimilarities for a
variant of Dybvig et al.'s calculus of multi-prompted
delimited-control operators with dynamic prompt generation. The
reasoning principles that we obtain generalize and advance the
existing techniques for establishing program equivalence in calculi
with single-prompted delimited control.
The basic theory that we develop is presented using Madiot et al.'s
framework that allows for smooth integration and composition of up-to
techniques facilitating bisimulation proofs. We also generalize the
framework in order to express environmental bisimulations that support
equivalence proofs of evaluation contexts representing
continuations. This change leads to a novel and powerful up-to
technique enhancing bisimulation proofs in the presence of control
operators.
delimited continuation
dynamic prompt generation
contextual equivalence
environmental bisimulation
up-to technique
9:1-9:17
Regular Paper
Andrés
Aristizábal
Andrés Aristizábal
Dariusz
Biernacki
Dariusz Biernacki
Sergueï
Lenglet
Sergueï Lenglet
Piotr
Polesiuk
Piotr Polesiuk
10.4230/LIPIcs.FSCD.2016.9
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental bisimulations for delimited-control operators with dynamic prompt generation. Research Report RR-8905, Inria, Nancy, France, April 2016. Available at URL: http://hal.inria.fr/hal-01305137.
http://hal.inria.fr/hal-01305137
Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In Xavier Leroy, editor, Proceedings of the Thirty-First Annual ACM Symposium on Principles of Programming Languages, pages 64-76, Venice, Italy, January 2004. ACM Press.
Nick Benton and Vasileios Koutavas. A mechanized bisimulation for the nu-calculus. Technical Report MSR-TR-2008-129, Microsoft Research, September 2008.
Dariusz Biernacki and Olivier Danvy. A simple proof of a folklore theorem about delimited control. Journal of Functional Programming, 16(3):269-280, 2006.
Dariusz Biernacki and Sergueï Lenglet. Applicative bisimulations for delimited-control operators. In Lars Birkedal, editor, Foundations of Software Science and Computation Structures, 15th International Conference (FOSSACS'12), volume 7213 of Lecture Notes in Computer Science, pages 119-134, Tallinn, Estonia, March 2012. Springer.
Dariusz Biernacki and Sergueï Lenglet. Normal form bisimulations for delimited-control operators. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming, 13th International Symposium (FLOPS'12), volume 7294 of Lecture Notes in Computer Science, pages 47-61, Kobe, Japan, May 2012. Springer.
Dariusz Biernacki and Sergueï Lenglet. Environmental bisimulations for delimited-control operators. In Chung-chieh Shan, editor, Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS'13), volume 8301 of Lecture Notes in Computer Science, pages 333-348, Melbourne, VIC, Australia, December 2013. Springer.
Dariusz Biernacki and Piotr Polesiuk. Logical relations for coherence of effect subtyping. In Thorsten Altenkirch, editor, Typed Lambda Calculi and Applications, 13th International Conference, TLCA 2015, volume 38 of Leibniz International Proceedings in Informatics, pages 107-122, Warsaw, Poland, July 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151-160, Nice, France, June 1990. ACM Press.
Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5):477-528, 2012.
R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. A monadic framework for delimited continuations. Journal of Functional Programming, 17(6):687-730, 2007.
Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180-190, San Diego, California, January 1988. ACM Press.
Andrzej Filinski. Representing monads. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 446-457, Portland, Oregon, January 1994. ACM Press.
Matthew Flatt, Gang Yu, Robert Bruce Findler, and Matthias Felleisen. Adding delimited and composable control to a production programming environment. In Norman Ramsey, editor, Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP'07), pages 165-176, Freiburg, Germany, September 2007. ACM Press.
Carl Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Simon Peyton Jones, editor, Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pages 12-23, La Jolla, California, June 1995. ACM Press.
Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. The marriage of bisimulations and Kripke logical relations. In John Field and Michael Hicks, editors, Proceedings of the Thirty-Ninth Annual ACM Symposium on Principles of Programming Languages, pages 59-72, Philadelphia, PA, USA, January 2012. ACM Press.
Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. A logical step forward in parametric bisimulations. Technical Report MPI-SWS-2014-003, Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany, January 2014.
Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Olin Shivers, editor, Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming (ICFP'03), pages 177-188, Uppsala, Sweden, August 2003. ACM Press.
Oleg Kiselyov. Delimited control in OCaml, abstractly and concretely: System description. In Matthias Blume and German Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, volume 6009 of Lecture Notes in Computer Science, pages 304-320, Sendai, Japan, April 2010. Springer.
Ikuo Kobori, Yukiyoshi Kameyama, and Oleg Kiselyov. ATM without tears: prompt-passing style transformation for typed delimited-control operators. In Olivier Danvy, editor, 2015 Workshop on Continuations: Pre-proceedings, London, UK, April 2015.
Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. From applicative to environmental bisimulation. In Michael Mislove and Joël Ouaknine, editors, Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXVII), volume 276 of Electronic Notes in Theoretical Computer Science, pages 215-235, Pittsburgh, PA, USA, May 2011.
Vasileios Koutavas and Mitchell Wand. Bisimulations for untyped imperative objects. In Peter Sestoft, editor, 15th European Symposium on Programming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 146-161, Vienna, Austria, March 2006. Springer.
Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, Proceedings of the 33rd Annual ACM Symposium on Principles of Programming Languages, pages 141-152, Charleston, SC, USA, January 2006. ACM Press.
Jean-Marie Madiot. Higher-Order Languages: Dualities and Bisimulation Enhancements. PhD thesis, Université de Lyon and Università di Bologna, 2015.
Jean-Marie Madiot, Damien Pous, and Davide Sangiorgi. Bisimulations up-to: Beyond first-order transition systems. In Paolo Baldan and Daniele Gorla, editors, 25th International Conference on Concurrency Theory, volume 8704 of Lecture Notes in Computer Science, pages 93-108, Rome, Italy, September 2014. Springer.
Adrien Piérard and Eijiro Sumii. A higher-order distributed calculus with name creation. In Proceedings of the 27th IEEE Symposium on Logic in Computer Science (LICS 2012), pages 531-540, Dubrovnik, Croatia, June 2012. IEEE Computer Society Press.
Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In Andrew Gordon and Andrew Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227-273. Publications of the Newton Institute, Cambridge University Press, 1998.
Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction, chapter 6, pages 233-289. Cambridge University Press, 2011.
Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1):1-69, January 2011.
Eijiro Sumii. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, CSL'09, volume 5771 of Lecture Notes in Computer Science, pages 455-469, Coimbra, Portugal, September 2009. Springer.
Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. Theoretical Computer Science, 375(1-3):169-192, 2007.
Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5), 2007.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Complexity of Acyclic Term Graph Rewriting
Term rewriting has been used as a formal model to reason about the
complexity of logic, functional, and imperative programs. In contrast
to term rewriting, term graph rewriting permits sharing of
common sub-expressions, and consequently is able to capture more
closely reasonable implementations of rule based languages. However,
the automated complexity analysis of term graph rewriting has received
little to no attention.
With this work, we provide first steps towards overcoming this
situation. We present adaptions of two prominent complexity techniques
from term rewriting, viz, the interpretation method and
dependency tuples. Our adaptions are non-trivial, in the sense
that they can observe not only term but also graph structures, i.e.
take sharing into account. In turn, the developed methods allow us to
more precisely estimate the runtime complexity of programs where
sharing of sub-expressions is essential.
Program Analysis
Graph Rewriting
Complexity Analysis
10:1-10:18
Regular Paper
Martin
Avanzini
Martin Avanzini
Georg
Moser
Georg Moser
10.4230/LIPIcs.FSCD.2016.10
M. Avanzini and U. Dal Lago. On Sharing, Memoization, and Polynomial Time. IC, 2015.
M. Avanzini, U. Dal Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Proc. of \nth20 ICFP, pages 152-164. ACM, 2015.
M. Avanzini, N. Eguchi, and G. Moser. A new Order-theoretic Characterisation of the Polytime Computable Functions. TCS, 585:3-24, 2015.
M. Avanzini and G. Moser. A Combination Framework for Complexity. IC, 2015.
M. Avanzini, G. Moser, and M. Schaper. TcT: Tyrolean Complexity Tool. In Proc. of \nnd22 TACAS, LNCS, 2016.
M. Avanzini, C. Sternagel, and R. Thiemann. Certification of Complexity Proofs using CeTA. In Proc. of \nth26 RTA, volume 36 of LIPIcs, pages 23-39, 2015.
E. Barendsen. Term Graph Rewriting. In Term Rewriting Systems, volume 55 of CTTCS, chapter 13, pages 712-743. Cambridge University Press, 2003.
G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with Polynomial Interpretation Termination Proof. JFP, 11(1):33-53, 2001.
G. Bonfante and B. Guillaume. Non-simplifying Graph Rewriting Termination. In Proc. of \nth7 TERMGRAPH, EPTCS, pages 4-16, 2013.
G. Bonfante, J.-Y. Marion, and J.-Y. Moyen. Quasi-interpretations: A Way to Control Resources. TCS, 412(25):2776-2796, 2011.
M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Proc. of \nth20 TACAS, volume 8413 of LNCS, pages 140-155, 2014.
H. J. Sander Bruggink, B. König, and H. Zantema. Termination Analysis for Graph Transformation Systems. In Proc. of \nth8 IFIP TC 1/WG 2.2, TCS, volume 8705 of LNCS, pages 179-194, 2014.
H.J.S. Bruggink, B. König, D. Nolte, and H. Zantema. Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings. In Proc. of \nth8 ICGT, volume 9151 of LNCS, pages 52-68, 2015.
N. Dershowitz. Termination Dependencies. In Proc. of \nth6 WST, pages 28-30. Universidad Politécnica de Valencia, 2003. Technical Report DSIC-II 03.
F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder. Inferring Lower Bounds for Runtime Complexity. In Proc. of \nth26 RTA, LIPIcs, pages 334-349, 2015.
J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic Evaluation Graphs and Term Rewriting: A General Methodology for Analyzing Logic Programs. In Proc. of \nth14 PPDP, pages 1-12. ACM, 2012.
S. Gimenez and G. Moser. The Complexity of Interaction. In Proc. of \nrd43 POPL, pages 243-255. ACM, 2016.
Y. Lafont. Interaction nets. In Proc. of \nth17 POPL, pages 95-108. ACM, 1990.
A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl. Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. In Proc. of \nth4 CAI, volume 6742 of LNCS, pages 1-20, 2011.
G. Moser. Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. CoRR, abs/0907.5527, 2009. Habilitation Thesis.
G. Moser. KBOs, Ordinals, Subrecursive Hierarchies and All That. JLC, 2014. advance access.
G. Moser and A. Schnabl. Proving Quadratic Derivational Complexities using Context Dependent Interpretations. In Proc. of \nth19 RTA, volume 5117 of LNCS, pages 276-290, 2008.
L. Noschinski, F. Emmes, and J. Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. JAR, 51(1):27-56, 2013.
M. Perrinel. On Context Semantics and Interaction Nets. In Proc. of Joint \nrd23 CSL and \nth29 LICS, page 73. ACM, 2014.
D. Plump. Simplification orders for term graph rewriting. In Proc. 22nd MFCS, volume 1295 of LNCS, pages 458-467, 1997.
D. Plump. Essentials of Term Graph Rewriting. ENTCS, 51:277-289, 2001.
S. L. Peyton Jones. The Implementation of Functional Languages. Prentice-Hall International, 1987.
M. Schaper. A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems. Master’s thesis, University of Innsbruck, Austria, 2014. URL: http://cl-informatik.uibk.ac.at/users/c7031025/publications/masterthesis.pdf.
http://cl-informatik.uibk.ac.at/users/c7031025/publications/masterthesis.pdf
J. Waldmann. Matrix Interpretations on Polyhedral Domains. In Proc. of \nth26 RTA, volume 36 of LIPIcs, pages 318-333, 2015.
H. Zankl and M. Korp. Modular Complexity Analysis for Term Rewriting. LMCS, 10(1:19):1-33, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Nominal Narrowing
Nominal unification is a generalisation of first-order unification
that takes alpha-equivalence into account. In this paper, we study
nominal unification in the context of equational theories. We
introduce nominal narrowing and design a general nominal E-unification
procedure, which is sound and complete for a wide class of equational
theories. We give examples of application.
Nominal Rewriting
Nominal Unification
Matching
Narrowing
Equational Theories
11:1-11:17
Regular Paper
Mauricio
Ayala-Rincón
Mauricio Ayala-Rincón
Maribel
Fernández
Maribel Fernández
Daniele
Nantes-Sobrinho
Daniele Nantes-Sobrinho
10.4230/LIPIcs.FSCD.2016.11
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic
Curry-Howard isomorphism makes it possible to obtain functional
programs from proofs in logic. We analyse the problem of program
synthesis for ML programs with algebraic types and relate it to the
proof search problems in appropriate logics. The problem of synthesis
for closed programs is easily equivalent to the proof construction in
intuitionistic propositional logic and thus fits in the class of
PSPACE-complete problems. We focus further attention on the synthesis
problem relative to a given external library of functions. It turns
out that the problem is undecidable for unbounded instantiation in
ML. However its restriction to instantiations with atomic types
only results in a case equivalent to proof search in a restricted
fragment of intuitionistic first-order logic, being the core of
Sigma_1 level of the logic in the Mints hierarchy. This results in
EXPSPACE-completeness for this special case of the ML program
synthesis problem.
ML
program synthesis
12:1-12:16
Regular Paper
Marcin
Benke
Marcin Benke
Aleksy
Schubert
Aleksy Schubert
Daria
Walukiewicz-Chrzaszcz
Daria Walukiewicz-Chrzaszcz
10.4230/LIPIcs.FSCD.2016.12
Lennart Augustsson, 2005. URL: https://github.com/augustss/djinn.
https://github.com/augustss/djinn
Coq Development Team. The Coq Proof Assistant Reference Manual V8.4, March 2012. URL: http://coq.inria.fr/distrib/V8.4/refman/.
http://coq.inria.fr/distrib/V8.4/refman/
Thierry Coquand and Gerard Huet. The calculus of constructions. Information and Computation, pages 95-120, 1988.
Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 207-212, New York, NY, USA, 1982. ACM.
Edsger Wybe Dijkstra. A Discipline of Programming. Prentice Hall, 1976.
Catherine Dubois. Proving ML type soundness within Coq. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14-18, 2000 Proceedings, pages 126-144, Berlin, Heidelberg, 2000. Springer.
Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded Combinatory Logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 243-258, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
J.-Y. Girard. Interprétation fonctionelle et élimination des coupures dans l'arithmetique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.
Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29-60, 1969.
Pierre Letouzey. Coq Extraction, an Overview. In C. Dimitracopoulos A. Beckmann and B. Löwe, editors, Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, volume 5028 of Lecture Notes in Computer Science. Springer-Verlag, 2008.
Samuel Linial and E. L. Post. Recursive unsolvability of the deducibility, Tarski’s completeness, and independence of axioms problems of propositional calculus. Bulletin of the American Mathematical Society, vol. 55, p. 50, 1949. Abstract.
Per Martin-Löf. Constructive mathematics and computer programming. In Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-175. North-Holland, 1982.
Marvin L. Minsky. Recursive unsolvability of Post’s problem of "Tag" and other topics in theory of Turing machines. Annals of Mathematics, 74(3):437-455, 1961.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Springer, 2002.
Christine Paulin-Mohring. Fω’s programs from proofs in the calculus of constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages. ACM Press, 1989.
J. C. Reynolds. Towards a theory of type structure. In Ehring et al., editor, Programming Symposium, Proceedings Colloque Sur La Programmation, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer, 1974.
Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski. On the Mints hierarchy in first-order intuitionistic logic. In A. Pitts, editor, Foundations of Software Science and Computation Structures 2015, volume 9034 of Lecture Notes in Computer Science, pages 451-465. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_29.
http://dx.doi.org/10.1007/978-3-662-46678-0_29
Helmut Schwichtenberg. The MINLOG system. URL: http://www.mathematik.uni-muenchen.de/~logik/minlog/.
http://www.mathematik.uni-muenchen.de/~logik/minlog/
W. E. Singletary. Many-one degrees associated with partial propositional calculi. Notre Dame J. Formal Logic, 15(2):335-343, 04 1974.
M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149. Elsevier, 2006.
Richard Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67-72, 1979.
Nicholas Wirth. Systematic Programming: An Introduction. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1973.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Classical Extraction in Continuation Models
We use the control features of continuation models to interpret proofs
in first-order classical theories. This interpretation is suitable for
extracting algorithms from proofs of Pi^0_2 formulas. It is
fundamentally different from the usual direct interpretation, which is
shown to be equivalent to Friedman's trick. The main difference is
that atomic formulas and natural numbers are interpreted as distinct
objects. Nevertheless, the control features inherent to the
continuation models permit extraction using a special "channel" on
which the extracted value is transmitted at toplevel without unfolding
the recursive calls. We prove that the technique fails in Scott
domains, but succeeds in the refined setting of Laird's bistable
bicpos, as well as in game semantics.
Extraction
Classical Logic
Control Operators
Game Semantics
13:1-13:17
Regular Paper
Valentin
Blot
Valentin Blot
10.4230/LIPIcs.FSCD.2016.13
Samson Abramsky, Kohei Honda, and Guy McCusker. A Fully Abstract Game Semantics for General References. In 13th Annual IEEE Symposium on Logic in Computer Science, pages 334-344. IEEE Computer Society, 1998.
Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full Abstraction for PCF. Information and Computation, 163(2):409-470, 2000.
Roberto Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.
Stefano Berardi, Marc Bezem, and Thierry Coquand. On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic, 63(2):600-622, 1998.
Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg. Refined program extraction from classical proofs. Annals of Pure and Applied Logic, 114(1-3):3-25, 2002.
Ulrich Berger and Paulo Oliva. Modified bar recursion and classical dependent choice. In Logic Colloquium 2001, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, volume 20 of Lecture Notes in Logic, pages 89-107. A K Peters, Ltd., 2005.
Valentin Blot and Colin Riba. On Bar Recursion and Choice in a Classical Setting. In 11th Asian Symposium on Programming Languages and Systems, volume 8301 of Lecture Notes in Computer Science, pages 349-364. Springer, 2013.
Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert Müller and Dana Scott, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21-27. Springer, 1978.
Timothy Griffin. A Formulae-as-Types Notion of Control. In 17th Symposium on Principles of Programming Languages, pages 47-58. ACM Press, 1990.
Russ Harmer. Games and full abstraction for non-deterministic languages. PhD thesis, Imperial College London (University of London), 1999.
Hugo Herbelin. On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. In 7th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Mathematics, pages 209-220. Springer, 2005.
Martin Hofmann and Thomas Streicher. Completeness of Continuation Models for λμ-Calculus. Information and Computation, 179(2):332-355, 2002.
Martin Hyland and Luke Ong. On Full Abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000.
Stephen Cole Kleene. On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic, 10(4):109-124, 1945.
Jean-Louis Krivine. Dependent choice, `quote' and the clock. Theoretical Computer Science, 308(1-3):259-276, 2003.
Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009.
Yves Lafont, Bernhard Reus, and Thomas Streicher. Continuations Semantics or Expressing Implication by Negation. Technical Report 93-21, Ludwig-Maximilians-Universität, München, 1993.
James Laird. Full Abstraction for Functional Languages with Control. In 12th Annual IEEE Symposium on Logic in Computer Science, pages 58-67. IEEE Computer Society, 1997.
James Laird. Bistable Biorders: A Sequential Domain Theory. Logical Methods in Computer Science, 3(2), 2007.
Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science, 7(2), 2011.
Hanno Nickau. Hereditarily Sequential Functionals. In Third International Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, pages 253-264. Springer, 1994.
Paulo Oliva and Thomas Streicher. On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundamenta Informaticae, 84(2):207-220, 2008.
Michel Parigot. λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In 3rd International Conference on Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer, 1992.
Christophe Raffalli. Getting results from programs extracted from classical proofs. Theoretical Computer Science, 323(1-3):49-70, 2004.
Peter Selinger. Control categories and duality: on the categorical semantics of the λμ calculus. Mathematical Structures in Computer Science, 11(2):207-260, 2001.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Proving Correctness of Logically Decorated Graph Rewriting Systems
We first introduce the notion of logically decorated rewriting systems where the left-hand sides are endowed with logical formulas which help to express positive as well as negative application conditions, in addition to classical pattern-matching. These systems are defined using graph structures and an extension of combinatory propositional
dynamic logic, CPDL, with restricted universal programs, called C2PDL. In a second step, we tackle the problem of proving the correctness of logically decorated graph rewriting systems by using a Hoare-like calculus. We introduce a notion of specification defined as a tuple (Pre, Post, R, S) with Pre and Post being formulas of C2PDL, R a rewriting system and S a rewriting strategy. We provide a sound calculus which infers proof obligations of the considered specifications and establish the decidability of the verification problem of the (partial) correctness of the considered specifications.
Graph Rewriting
Hoare Logic,Combinatory PDL
Rewrite Strategies
Program Verification
14:1-14:15
Regular Paper
Jon Haël
Brenas
Jon Haël Brenas
Rachid
Echahed
Rachid Echahed
Martin
Strecker
Martin Strecker
10.4230/LIPIcs.FSCD.2016.14
Carlos E. Alchourrón, Peter Gärdenfors, and David Makinson. On the logic of theory change: Partial meet contraction and revision functions. J. Symb. Log., 50(2):510-530, 1985. URL: http://dx.doi.org/10.2307/2274239.
http://dx.doi.org/10.2307/2274239
Carlos Areces and Balder ten Cate. Hybrid logics. In Studies in Logic and Practical Reasoning, volume 3, pages 821-868. Elsevier, 2007.
Philippe Balbiani, Rachid Echahed, and Andreas Herzig. A dynamic logic for termgraph rewriting. In 5th International Conference on Graph Transformations (ICGT), volume 6372 of Lecture Notes in Computer Science, pages 59-74. Springer, 2010.
Jon Haël Brenas, Rachid Echahed, and Martin Strecker. A Hoare-like calculus using the SROIQ σ logic on transformations of graphs. In Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, pages 164-178, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44602-7_14.
http://dx.doi.org/10.1007/978-3-662-44602-7_14
Jon Hael Brenas, Rachid Echahed, and Martin Strecker. C2PDLS: A combination of combinatory and converse PDL with substitutions. 2015. URL: http://lig-membres.imag.fr/echahed/c2pdls.pdf.
http://lig-membres.imag.fr/echahed/c2pdls.pdf
Ricardo Caferra, Rachid Echahed, and Nicolas Peltier. A term-graph clausal logic: Completeness and incompleteness results. Journal of Applied Non-classical Logics, 18(4):373-411, 2008.
Rachid Echahed. Inductively sequential term-graph rewrite systems. In 4th International Conference on Graph Transformations, ICGT, volume 5214 of Lecture Notes in Computer Science, pages 84-98. Springer, 2008.
Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194-211, 1979. URL: http://dx.doi.org/10.1016/0022-0000(79)90046-1.
http://dx.doi.org/10.1016/0022-0000(79)90046-1
Annegret Habel, Reiko Heckel, and Gabriele Taentzer. Graph grammars with negative application conditions. Fundam. Inform., 26(3/4):287-313, 1996. URL: http://dx.doi.org/10.3233/FI-1996-263404.
http://dx.doi.org/10.3233/FI-1996-263404
Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. MSCS, 19:245-296, 2009.
C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: http://dx.doi.org/10.1145/363235.363259.
http://dx.doi.org/10.1145/363235.363259
Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, and Greta Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, volume 3210 of Lecture Notes in Computer Science, pages 160-174. Springer Berlin / Heidelberg, 2004. URL: http://www.cs.umass.edu/~immerman/pub/cslPaper.pdf.
http://www.cs.umass.edu/~immerman/pub/cslPaper.pdf
Kazuhiro Inaba, Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, and Keisuke Nakano. Graph-transformation verification using monadic second-order logic. In Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pages 17-28, 2011. URL: http://dx.doi.org/10.1145/2003476.2003482.
http://dx.doi.org/10.1145/2003476.2003482
Barbara König and Javier Esparza. Verification of graph transformation systems with context-free specifications. In Graph Transformations - 5th International Conference, ICGT 2010, Enschede, The Netherlands, September 27 - October 2, 2010. Proceedings, pages 107-122, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15928-2_8.
http://dx.doi.org/10.1007/978-3-642-15928-2_8
Solomon Passy and Tinko Tinchev. An essay in combinatory dynamic logic. Inf. Comput., 93(2):263-332, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90026-X.
http://dx.doi.org/10.1016/0890-5401(91)90026-X
Christopher M. Poskitt and Detlef Plump. Verifying monadic second-order properties of graph programs. In Graph Transformation - 7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014. Proceedings, pages 33-48, 2014. URL: http://dx.doi.org/10.1007/978-3-319-09108-2_3.
http://dx.doi.org/10.1007/978-3-319-09108-2_3
Arend Rensink, Ákos Schmidt, and Dániel Varró. Model checking graph transformations: A comparison of two approaches. In Graph Transformations, Second International Conference, ICGT 2004, Rome, Italy, September 28 - October 2, 2004, Proceedings, pages 226-241, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30203-2_17.
http://dx.doi.org/10.1007/978-3-540-30203-2_17
Grzegorz Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, 1997.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable
Working in the untyped lambda calculus, we study Morris's
lambda-theory H+. Introduced in 1968, this is the original
extensional theory of contextual equivalence. On the syntactic side,
we show that this lambda-theory validates the omega-rule, thus
settling a long-standing open problem.On the semantic side, we
provide sufficient and necessary conditions for relational graph
models to be fully abstract for H+. We show that a relational graph
model captures Morris's observational preorder exactly when it is
extensional and lambda-Konig. Intuitively, a model is lambda-Konig
when every lambda-definable tree has an infinite path which is
witnessed by some element of the model.
Both results follow from a weak separability property enjoyed by
terms differing only because of some infinite eta-expansion,
which is proved through a refined version of the Böhm-out technique.
Lambda calculus
relational models
fully abstract
Böhm-out
omega-rule
15:1-15:18
Regular Paper
Flavien
Breuvart
Flavien Breuvart
Giulio
Manzonetto
Giulio Manzonetto
Andrew
Polonsky
Andrew Polonsky
Domenico
Ruoppolo
Domenico Ruoppolo
10.4230/LIPIcs.FSCD.2016.15
H.P. Barendregt. The lambda-calculus, its syntax and semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984.
C. Berline. From computation to foundations via functions and application: The λ-calculus and its webbed models. Theoretical Computer Science, 249(1):81-161, 2000.
C. Böhm. Alcune proprietà delle forme β-η-normali nel λ-K-calcolo. Pub. INAC, 696, 1968.
F. Breuvart. On the characterization of models of ℋ^*. In T. Henzinger and D. Miller, editors, Joint Meeting CSL-LICS'14, pages 24:1-24:10. ACM, 2014.
A. Bucciarelli, T. Ehrhard, and G. Manzonetto. Not enough points is enough. In CSL'07, volume 4646 of Lecture Notes in Comput. Sci., pages 298-312. Springer, 2007.
M. Coppo, M. Dezani, and M. Zacchi. Type theories, normal forms and D_∞-lambda-models. Inf. Comput., 72(2):85-116, 1987.
M. Dezani-Ciancaglini and E. Giovannetti. From Bohm’s theorem to observational equivalences: an informal account. Electr. Notes Theor. Comput. Sci., 50(2):83-116, 2001.
T. Ehrhard and L. Regnier. The differential λ-calculus. Th. Comp. Sci., 309(1):1-41, 2003.
T. Ehrhard and L. Regnier. Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms. In CiE, volume 3988 of Lecture Notes in Comput. Sci., pages 186-197, 2006. URL: http://dx.doi.org/10.1007/11780342_20.
http://dx.doi.org/10.1007/11780342_20
E. Engeler. Algebras and combinators. Algebra Universalis, 13(3):389-392, 1981.
P. Di Gianantonio, G. Franco, and F. Honsell. Game semantics for untyped λ β η-calculus. In TLCA'99, volume 1581 of Lecture Notes in Comput. Sci., pages 114-128. Springer, 1999.
R. Hindley and G. Longo. Lambda-calculus models and extensionality. Z. Math. Logik Grundlag. Math., 26(4):289-310, 1980.
J.M.E. Hyland. A survey of some useful partial order relations on terms of the λ-calculus. In Lambda-Calculus and Comp. Sci. Th., volume 37 of LNCS, pages 83-95. Springer, 1975.
J.M.E. Hyland. A syntactic characterization of the equality in some models for the λ-calculus. J. London Math. Soc. (2), 12(3):361-370, 1975/76.
J.M.E. Hyland, M. Nagayama, J. Power, and G. Rosolini. A category theoretic formulation for Engeler-style models of the untyped λ-calculus. Electr. Notes in TCS, 161:43-57, 2006.
J.-J. Lévy. Le lambda calcul - notes du cours, 2005. In French. URL: http://pauillac.inria.fr/~levy/courses/X/M1/lambda/dea-spp/jjl.pdf.
http://pauillac.inria.fr/~levy/courses/X/M1/lambda/dea-spp/jjl.pdf
S. Lusin and A. Salibra. The lattice of λ-theories. J. Log. Comput., 14(3):373-394, 2004.
G. Manzonetto. A general class of models of ℋ^⋆. In MFCS 2009, volume 5734 of Lecture Notes in Comput. Sci., pages 574-586. Springer, 2009.
G. Manzonetto. What is a categorical model of the differential and the resource λ-calculi? Mathematical Structures in Computer Science, 22(3):451-520, 2012.
G. Manzonetto and D. Ruoppolo. Relational graph models, Taylor expansion and extensionality. Electr. Notes Theor. Comput. Sci., 308:245-272, 2014.
J.H. Morris. Lambda calculus models of programming languages. PhD thesis, MIT, 1968.
L. Paolini, M. Piccolo, and S. Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science, 2015. URL: http://dx.doi.org/10.1017/S0960129515000316.
http://dx.doi.org/10.1017/S0960129515000316
S. Ronchi Della Rocca and L. Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.
D. Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Math., pages 97-136. Springer, 1972.
P. Severi and F.J. de Vries. The infinitary lambda calculus of the infinite eta Böhm trees. To appear in Math. Struct. Comp. Sci., 2016.
C.P. Wadsworth. The relation between computational and denotational properties for Scott’s D_∞-models of the lambda-calculus. SIAM J. Comput., 5(3):488-521, 1976.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Modular Focused Proof Systems for Intuitionistic Modal Logics
Focusing is a general technique for syntactically compartmentalizing
the non-deterministic choices in a proof system, which not only
improves proof search but also has the representational benefit of
distilling sequent proofs into synthetic normal forms. However, since
focusing is usually specified as a restriction of the sequent
calculus, the technique has not been transferred to logics that lack a
(shallow) sequent presentation, as is the case for some of the logics
of the modal cube. We have recently extended the focusing technique
to classical nested sequents, a generalization of ordinary sequents.
In this work we further extend focusing to intuitionistic nested
sequents, which can capture all the logics of the intuitionistic S5
cube in a modular fashion. We present an internal cut-elimination
procedure for the focused system which in turn is used to show its
completeness.
intuitionistic modal logic
focusing
proof search
cut elimination
nested sequents
16:1-16:18
Regular Paper
Kaustuv
Chaudhuri
Kaustuv Chaudhuri
Sonia
Marin
Sonia Marin
Lutz
Straßburger
Lutz Straßburger
10.4230/LIPIcs.FSCD.2016.16
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297-347, 1992. URL: http://dx.doi.org/10.1093/logcom/2.3.297.
http://dx.doi.org/10.1093/logcom/2.3.297
Arnon Avron. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: from foundations to applications: European logic colloquium, pages 1-32. Clarendon Press, 1996.
Taus Brock-Nannestad and Carsten Schürmann. Focused natural deduction. In LPAR 17, volume 6397 of LNCS, pages 157-171, Yogyakarta, Indonesia, 2010. Springer. URL: http://dx.doi.org/10.1007/978-3-642-16242-8_12.
http://dx.doi.org/10.1007/978-3-642-16242-8_12
Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551-577, 2009.
Kai Brünnler and Lutz Straßburger. Modular sequent systems for modal logic. In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'09, volume 5607 of LNCS, pages 152-166. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02716-1_12.
http://dx.doi.org/10.1007/978-3-642-02716-1_12
Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The focused calculus of structures. In CSL, (LIPIcs), pages 159-173. Schloss Dagstuhl-LZI, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159.
http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159
Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Focused and synthetic nested sequents. In Bart Jacobs and Christof Löding, editors, FoSSaCS, April 2016. To appear.
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J. of Autom. Reasoning, 40(2-3):133-177, 2008. URL: http://dx.doi.org/10.1007/s10817-007-9091-0.
http://dx.doi.org/10.1007/s10817-007-9091-0
François Lamarche. On the algebra of structural contexts. Technical report, INRIA, 2006. Available at https://hal.inria.fr/inria-00099461; to appear in MSCS.
https://hal.inria.fr/inria-00099461
Olivier Laurent. A proof of the focalization property in linear logic. Unpublished note, 2004.
Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. URL: http://dx.doi.org/10.1016/j.tcs.2009.07.041.
http://dx.doi.org/10.1016/j.tcs.2009.07.041
Sonia Marin and Lutz Straßburger. Label-free modular systems for classical and intuitionistic modal logics. In Advances in Modal Logic (AIML-10), 2014.
Sean McLaughlin and Frank Pfenning. Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic. In 15th LPAR, volume 5330 of LNCS, pages 174-181, 2008.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991.
Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5-6):507-544, 2005. URL: http://dx.doi.org/10.1007/s10992-005-2267-3.
http://dx.doi.org/10.1007/s10992-005-2267-3
Gordon D. Plotkin and Colin Stirling. A framework for intuitionistic modal logics. In 1st Conference on Theoretical Aspects of Reasoning about Knowledge, pages 399-406. Morgan Kaufmann, 1986.
Jason Reed and Frank Pfenning. Focus-preserving embeddings of substructural logics in intuitionistic logic. Draft manuscript, January 2010.
Gisèle Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico dell' Università Politecnica di Torino, 42(3):179-194, 1984.
Robert J. Simmons. Structural focalization. ACM Trans. Comput. Log., 15(3):21:1-21:33, 2014. URL: http://dx.doi.org/10.1145/2629678.
http://dx.doi.org/10.1145/2629678
Alex Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994.
Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In 16th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), volume 7794 of LNCS, pages 209-224. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37075-5_14.
http://dx.doi.org/10.1007/978-3-642-37075-5_14
Noam Zeilberger. Focusing and higher-order abstract syntax. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 359-369. ACM, 2008.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Independence of Markov’s Principle in Type Theory
In this paper, we show that Markov's principle is not derivable in
dependent type theory with natural numbers and one universe. One
tentative way to prove this would be to remark that Markov's principle
does not hold in a sheaf model of type theory over Cantor space, since
Markov's principle does not hold for the generic point of this model.
It is however not clear how to interpret the universe in a sheaf
model. Instead we design an extension of type theory, which
intuitively extends type theory by the addition of a generic point of
Cantor space. We then show the consistency of this extension by a
normalization argument. Markov's principle does not hold in this
extension, and it follows that it cannot be proved in type theory.
Forcing
Dependent type theory
Markov's Principle
Cantor Space
17:1-17:18
Regular Paper
Thierry
Coquand
Thierry Coquand
Bassel
Mannaa
Bassel Mannaa
10.4230/LIPIcs.FSCD.2016.17
Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Methods in Computer Science, 8(1):1-36, 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:29)2012.
http://dx.doi.org/10.2168/LMCS-8(1:29)2012
Peter Aczel. On relating type theories and set theories. In Thorsten Altenkirch, Bernhard Reus, and Wolfgang Naraschewski, editors, Types for Proofs and Programs: International Workshop, TYPES' 98 Kloster Irsee, Germany, March 27-31, 1998 Selected Papers, pages 1-18, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.
Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967.
L. E. J. Brouwer. Essentially negative properties. In A. Heyting, editor, Collected Works, volume I, pages 478 - 479. North-Holland, 1975.
Paul J Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 50(6):1143-1148, 12 1963.
Robert L. Constable and Scott Fraser Smith. Partial objects in constructive type theory. In Proceedings of Second IEEE Symposium on Logic in Computer Science, pages 183-193, 1987.
Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundamenta Informaticae, 100(1-4):43-52, 2010.
Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525-549, 2000.
Martin Hofmann and Thomas Streicher. Lifting grothendieck universes. unpublished note, publication year unknown. URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf
J.M.E. Hyland and C.-H.L. Ong. Modified realizability toposes and strong normalization proofs (extended abstract). In Typed Lambda Calculi and Applications, LNCS 664, pages 179-194. Springer-Verlag, 1993.
Alexei Kopylov and Aleksey Nogin. Markov’s principle for propositional type theory. In Laurent Fribourg, editor, Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris, France, September 10-13, 2001, Proceedings, pages 570-584, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg.
Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101-128. Amsterdam, North-Holland Pub. Co., 1959.
Kenneth Kunen. Set Theory: An Introduction to Independence Proofs, volume 102 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1980.
Maurice Margenstern. L’école constructive de Markov. Revue d'histoire des mathématiques, 1(2):271-305, 1995.
Per Martin-Löf. An intuitionistic theory of types. reprinted in Twenty-five years of constructive type theory, Oxford University Press, 1998, 127-172, 1972.
Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007.
Thomas Streicher. Universes in toposes. In Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis: Towards practicable foundations for constructive mathematics, pages 78-90. Oxford University Press, 2005.
William W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198-212, 1967.
Dirk van Dalen. An interpretation of intuitionistic analysis. Annals of Mathematical Logic, 13(1):1 - 43, 1978.
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38 - 94, 1994.
Chuangjie Xu and Martín Escardó. Universes in sheaf models. University of Birmingham, 2016.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On Undefined and Meaningless in Lambda Definability
We distinguish between undefined terms as used in lambda definability
of partial recursive functions and meaningless terms as used in
infinite lambda calculus for the infinitary terms models that
generalise the Bohm model. While there are uncountable many known
sets of meaningless terms, there are four known sets of undefined
terms. Two of these four are sets of meaningless terms.
In this paper we first present set of sufficient conditions for a set
of lambda terms to serve as set of undefined terms in lambda
definability of partial functions. The four known sets of undefined
terms satisfy these conditions.
Next we locate the smallest set of meaningless terms satisfying these
conditions. This set sits very low in the lattice of all sets of
meaningless terms. Any larger set of meaningless terms than this
smallest set is a set of undefined terms. Thus we find uncountably
many new sets of undefined terms.
As an unexpected bonus of our careful analysis of lambda definability
we obtain a natural modification, strict lambda-definability, which
allows for a Barendregt style of proof in which the representation of
composition is truly the composition of representations.
lambda calculus
lambda definability
partial recursive function
undefined term
meaningless term
18:1-18:15
Regular Paper
Fer-Jan
de Vries
Fer-Jan de Vries
10.4230/LIPIcs.FSCD.2016.18
H. P. Barendregt. Some extensional term models for combinatory logics and λ-calculi. PhD thesis, Univ. Utrecht, 1971.
H. P. Barendregt. A global representation of the recursive functions in the lambda-calculus. Theor. Comput. Sci., 3(2):225-242, 1976. URL: http://dx.doi.org/10.1016/0304-3975(76)90025-6.
http://dx.doi.org/10.1016/0304-3975(76)90025-6
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, Revised edition, 1984.
H.P. Barendregt. Solvability in lambda calculi. In M. Guillaume, editor, Colloque international de logique: Clermont-Ferrand, 1975, pages 209-219. Éditions du C.N.R.S., 1977.
H.P. Barendregt. Representing `undefined' in lambda calculus. J. Funct. Program., 2(3):367-374, 1992. URL: http://dx.doi.org/10.1017/S0956796800000447.
http://dx.doi.org/10.1017/S0956796800000447
A. Berarducci. Infinite λ-calculus and non-sensible models. In Logic and algebra (Pontignano, 1994), pages 339-377. Dekker, New York, 1996.
A. Berarducci and B. Intrigila. Church-Rosser lambda-theories, Infinite lambda-terms and consistency problems. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: from Foundations to Applications, pages 33-58. Oxford Science Publications, 1996. URL: http://www.dm.unipi.it/~berardu/Art/1996Church/CRtheories.pdf.
http://www.dm.unipi.it/~berardu/Art/1996Church/CRtheories.pdf
J. A. Bergstra and J. van de Pol. A calculus for four-valued sequential logic. Theor. Comput. Sci., 412(28):3122-3128, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.02.035.
http://dx.doi.org/10.1016/j.tcs.2011.02.035
A. Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345-363, 1936.
A. Church. The Calculi of Lambda Conversion. Princeton University Press, 1941.
H. B. Curry, J. R. Hindley, and J. P. Seldin. Combinatory Logic II. North-Holland, 1972.
G. Jacopini and M. Venturini-Zilli. Easy terms in the lambda-calculus. Fundamenta Informaticae, VIII(2):225-233, 1985.
J. R. Kennaway and F. J. de Vries. Infinitary rewriting. In Terese, editor, Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science, pages 668-711. Cambridge University Press, 2003.
J. R. Kennaway, V. van Oostrom, and F. J. de Vries. Meaningless terms in rewriting. Journal of Functional and Logic Programming, 1999(1), 1999. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html.
http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html
S. C. Kleene. λ-definability and recursiveness. Duke Math. J., 2(2):340-353, 06 1936. URL: http://dx.doi.org/10.1215/S0012-7094-36-00227-2.
http://dx.doi.org/10.1215/S0012-7094-36-00227-2
S. C. Kleene. On notation for ordinal numbers. J. Symb. Log., 3(4):150-155, 1938. URL: http://dx.doi.org/10.2307/2267778.
http://dx.doi.org/10.2307/2267778
Beata Konikowska, Andrzej Tarlecki, and Andrzej Blikle. A three-valued logic for software specification and validation. Fundam. Inform., 14(4):411-453, 1991.
G. Kreisel. Some reasons for generalising recursion theory. In R.O. Gandy and C.M.E. Yates, editors, Logic Colloquium 1969: proceedings of the summerschool and colloquium in mathematical logic, Manchester, August 1969, pages 139-189. North-Holland, 1971.
P. Severi and F. J. de Vries. Order Structures for Böhm-like models. In Computer Science Logic, volume 3634 of LNCS, pages 103-116. Springer-Verlag, 2005.
P. Severi and F. J. de Vries. Weakening the axiom of overlap in infinitary lambda calculus. In M. Schmidt-Schauß, editor, Proc. of the 22nd Int'l Conf. on Rewriting Techniques and Applications, May 30 - June 1, 2011, volume 10 of LIPIcs, pages 313-328. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2011.313.
http://dx.doi.org/10.4230/LIPIcs.RTA.2011.313
P. G. Severi and F. J. de Vries. Decomposing the lattice of meaningless sets in the infinitary lambda calculus. In L. D. Beklemishev and R. de Queiroz, editors, Proc. of the 18th Int'l Workshop on Logic, Language, Information and Computation (WoLLIC 2011), pages 210-227, 2011. URL: http://dx.doi.org/10.1007/978-3-642-20920-8_22.
http://dx.doi.org/10.1007/978-3-642-20920-8_22
A. M. Turing. Computability and λ-definability. J. Symb. Log., 2(4):153-163, 1937. URL: http://dx.doi.org/10.2307/2268280.
http://dx.doi.org/10.2307/2268280
A. M. Turing. The frakp-function in λ-K-conversion. J. Symb. Log., 2(4):164, 1937. URL: http://dx.doi.org/10.2307/2268281.
http://dx.doi.org/10.2307/2268281
A. Visser. Numerations, λ-calculus &arithmetic. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 259-284. Academic Press, 1980.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Intersection Type Unification Problem
The intersection type unification problem is an important component in
proof search related to several natural decision problems in
intersection type systems. It is unknown and remains open whether the
unification problem is decidable. We give the first nontrivial lower
bound for the problem by showing (our main result) that it is
exponential time hard. Furthermore, we show that this holds even under
rank 1 solutions (substitutions whose codomains are restricted to
contain rank 1 types). In addition, we provide a fixed-parameter
intractability result for intersection type matching (one-sided
unification), which is known to be NP-complete.
We place the intersection type unification problem in the context of
unification theory. The equational theory of intersection types can
be presented as an algebraic theory with an ACI (associative,
commutative, and idempotent) operator (intersection type) combined
with distributivity properties with respect to a second operator
(function type). Although the problem is algebraically natural and
interesting, it appears to occupy a hitherto unstudied place in the
theory of unification, and our investigation of the problem suggests
that new methods are required to understand the problem. Thus, for the
lower bound proof, we were not able to reduce from known results in
ACI-unification theory and use game-theoretic methods for two-player
tiling games.
Intersection Type
Equational Theory
Unification
Tiling
Complexity
19:1-19:16
Regular Paper
Andrej
Dudenhefner
Andrej Dudenhefner
Moritz
Martens
Moritz Martens
Jakob
Rehof
Jakob Rehof
10.4230/LIPIcs.FSCD.2016.19
S. Anantharaman, P. Narendran, and M. Rusinowitch. Acid-unification is NEXPTIME-decidable. In Mathematical Foundations of Computer Science 2003, pages 169-178. Springer, 2003.
S. Anantharaman, P. Narendran, and M. Rusinowitch. Unification Modulo ACUI Plus Distributivity Axioms. Journal of Automated Reasoning, 33(1):1-28, 2004.
F. Baader and P. Narendran. Unification of Concept Terms in Description Logics. Journal of Symbolic Computation, 31:277-305, 2001.
H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. URL: http://dx.doi.org/10.2307/2273659.
http://dx.doi.org/10.2307/2273659
H. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013.
G. Boudol and P. Zimmer. On type inference in the intersection type discipline. Electr. Notes Theor. Comput. Sci., 136:23-42, 2005. URL: http://dx.doi.org/10.1016/j.entcs.2005.06.016.
http://dx.doi.org/10.1016/j.entcs.2005.06.016
G. Castagna, K. Nguyen, Z. Xu, and P. Abate. Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction. In Principles of Programming Languages POPL 2015, pages 289-302. ACM, 2015.
W. Charatonik and L. Pacholski. Set constraints with projections are in NEXPTIME. In 35th Annual Symposium on Foundations of Computer Science, pages 642-653. IEEE, 1994. URL: http://dx.doi.org/10.1109/SFCS.1994.365727.
http://dx.doi.org/10.1109/SFCS.1994.365727
B. S. Chlebus. Domino-tiling games. Journal of Computer and System Sciences, 32(3):374-392, 1986.
M. Coppo and P. Giannini. Principal types and unification for a simple intersection type system. Inf. Comput., 122(1):70-96, 1995. URL: http://dx.doi.org/10.1006/inco.1995.1141.
http://dx.doi.org/10.1006/inco.1995.1141
M. Dezani-Ciancaglini and J. R. Hindley. Intersection Types for Combinatory Logic. Theoretical Computer Science, 100(2):303-324, 1992.
B. Düdder, M. Martens, and J. Rehof. Intersection Type Matching with Subtyping. In Proceedings of TLCA'13, Springer LNCS, 2013.
B. Düdder, M. Martens, J. Rehof, and P. Urzyczyn. Bounded Combinatory Logic. In Proceedings of CSL'12, volume 16 of LIPIcs, pages 243-258, 2012.
J. R. Hindley. The Simple Semantics for Coppo-Dezani-Sallé Types. In International Symposium on Programming, volume 137 of LNCS, pages 212-226. Springer, 1982.
J. R. Hindley and J. P. Seldin. Lambda-calculus and Combinators, an Introduction. Cambridge University Press, 2008.
A. J. Kfoury. Beta-reduction as unification. Banach Center Publications, 46(1):137-158, 1999.
A. J. Kfoury and J. B. Wells. Principality and Type Inference for Intersection Types Using Expansion Variables. Theor. Comput. Sci., 311(1-3):1-70, 2004.
T. Kurata and M. Takahashi. Decidable properties of intersection type systems. In TLCA, volume 902 of LNCS, pages 297-311. Springer, 1995.
J. Rehof and P. Urzyczyn. Finite Combinatory Logic with Intersection Types. In Proceedings of TLCA'11, volume 6690 of LNCS, pages 169-183. Springer, 2011.
J. Rehof and P. Urzyczyn. The Complexity of Inhabitation with Explicit Intersection. In Kozen Festschrift, volume 7230 of LNCS, pages 256-270. Springer, 2012.
S. Ronchi Della Rocca. Principal Type Scheme and Unification for Intersection Type Discipline. Theor. Comput. Sci., 59:181-209, 1988.
R. Statman. A finite model property for intersection types. In Proceedings Seventh Workshop on Intersection Types and Related Systems, ITRS 2014, Vienna, Austria, 18 July 2014., pages 1-9, 2015. URL: http://dx.doi.org/10.4204/EPTCS.177.1.
http://dx.doi.org/10.4204/EPTCS.177.1
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Computing Connected Proof(-Structure)s From Their Taylor Expansion
We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational
model is injective with respect to connected MELL proof-structures.
proof-nets
(differential) linear logic
relational model
Taylor expansion
20:1-20:18
Regular Paper
Giulio
Guerrieri
Giulio Guerrieri
Luc
Pellissier
Luc Pellissier
Lorenzo
Tortora de Falco
Lorenzo Tortora de Falco
10.4230/LIPIcs.FSCD.2016.20
V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical logic, 28(3):181-203, 1989.
V. Danos and L. Regnier. Proof-nets and the Hilbert space. In Advances in Linear Logic, pages 307-328. Cambridge University Press, 1995.
D. de Carvalho. The relational model is injective for Multiplicative Exponential Linear Logic. Preprint available at http://arxiv.org/abs/1502.02404, April 2015.
http://arxiv.org/abs/1502.02404
D. de Carvalho, M. Pagani, and L. Tortora de Falco. A semantic measure of the execution time in Linear Logic. Theoretical Computer Science, 412(20):1884-1902, 2011.
D. de Carvalho and L. Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakening). Ann. Pure Appl. Logic, 163(9):1210-1236, 2012.
T. Ehrhard. Finiteness spaces. Math. Struct. Comp. Science, 15(4):615-646, 2005.
T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003.
T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006.
T. Ehrhard and L. Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347-372, 2008.
H. Friedman. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 22-37. Springer Berlin, 1975.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987.
G. Guerrieri, L. Pellissier, and L. Tortora de Falco. Syntax, Taylor expansion and relational semantics of MELL proof-structures: an unusual approach. Technical report, 2016. Available at URL: http://logica.uniroma3.it/~tortora/mell.pdf.
http://logica.uniroma3.it/~tortora/mell.pdf
Y. Lafont. From Proof-Nets to Interaction Nets. In Advances in Linear Logic, pages 225-247. Cambridge University Press, 1995.
O. Laurent. Polarized proof-nets and λμ-calculus. Theor. Comp. Sci., 290(1):161-188, 2003.
D. Mazza and M. Pagani. The Separation Theorem for Differential Interaction Nets. In Proceedings of LPAR 2007, pages 393-407, 2007.
M. Pagani. The Cut-Elimination Thereom for Differential Nets with Boxes. In Proceedings of TLCA 2009, pages 219-233, 2009.
M. Pagani and C. Tasson. The Taylor Expansion Inverse Problem in Linear Logic. In Proceedings of LICS 2009, pages 222-231, 2009.
R. Statman. Completeness, invariance and λ-definability. J. Symb. Logic, 47(1):17-26, 1982.
L. Tortora de Falco. Obsessional Experiments For Linear Logic Proof-Nets. Mathematical Structures in Computer Science, 13(6):799-855, December 2003.
P. Tranquilli. Intuitionistic differential nets and lambda-calculus. Theoretical Computer Science, 412(20):1979-1997, 2011.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories
Cyclic data structures, such as cyclic lists, in functional
programming are tricky to handle because of their cyclicity. This
paper presents an investigation of categorical, algebraic, and
computational foundations of cyclic datatypes. Our framework of
cyclic datatypes is based on second-order algebraic theories of Fiore
et al., which give a uniform setting for syntax, types, and
computation rules for describing and reasoning about cyclic datatypes.
We extract the ``fold'' computation rules from the categorical
semantics based on iteration categories of Bloom and Esik. Thereby,
the rules are correct by construction. Finally, we prove strong
normalisation using the General Schema criterion for second-order
computation rules. Rather than the fixed point law, we particularly
choose Bekic law for computation, which is a key to obtaining strong
normalisation.
cyclic data structures
traced cartesian category
fixed point
functional programming
fold
21:1-21:18
Regular Paper
Makoto
Hamana
Makoto Hamana
10.4230/LIPIcs.FSCD.2016.21
Z. M. Ariola and S. Blom. Cyclic lambda calculi. In Theoretical Aspects of Computer Software, LNCS 1281, pages 77-106, 1997.
Z. M. Ariola and J. W. Klop. Equational term graph rewriting. Fundam. Inform., 26(3/4):207-240, 1996.
F. Blanqui. Termination and confluence of higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833, pages 47-61. Springer, 2000.
F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive data type systems. Theoretical Computer Science, 272:41-68, 2002.
S. L. Bloom and Z. Ésik. Iteration Theories - The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, 1993.
P. Buneman, M. F. Fernandez, and D. Suciu. UnQL: A query language and algebra for semistructured data based on structural recursion. VLDB J., 9(1):76-110, 2000.
C. Calcagno, P. Gardner, and U. Zarfaty. Context logic and tree update. In Proc. of POPL'05, pages 271-282, 2005. URL: http://dx.doi.org/10.1145/1040305.1040328.
http://dx.doi.org/10.1145/1040305.1040328
T. Coquand. Pattern matching with dependent types. In Proc. of the 3rd Work. on Types for Proofs and Programs, 1992.
J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In Typed Lambda Calculi and Applications, LNCS 902, pages 124-138, 1995.
A. Dovier, C. Piazza, and A. Policriti. An efficient algorithm for computing bisimulation equivalence. Theoretical Computer Science, 311:221-256, 2004. Issues 1-3.
Z. Ésik. Axiomatizing iteration categories. Acta Cybernetica, 14:65-82, 1999.
L. Fegaras and T. Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In POPL'96, pages 284-294, 1996. URL: http://dx.doi.org/10.1145/237721.237792.
http://dx.doi.org/10.1145/237721.237792
M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL'10, LNCS 6247, pages 320-335, 2010.
M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. of MFCS'10, LNCS 6281, pages 368-380, 2010.
M. Fiore and S. Staton. Substitution, jumps, and algebraic effects. In Proc. of LICS'14, 2014.
M. P. Fiore and M. D. Campos. The algebra of directed acyclic graphs. In Computation, Logic, Games, and Quantum Foundations, LNCS 7860, pages 37-51, 2013.
N. Ghani, M. Hamana, T. Uustalu, and V. Vene. Representing cyclic structures as nested datatypes. In Proc. of TFP'06, pages 173-188, 2006.
M. Hamana. Universal algebra for termination of higher-order rewriting. In Proc. of RTA'05, LNCS 3467, pages 135-149, 2005.
M. Hamana. Higher-order semantic labelling for inductive datatype systems. In Proc. of PPDP'07, pages 97-108. ACM Press, 2007. URL: http://dx.doi.org/10.1145/1273920.1273933.
http://dx.doi.org/10.1145/1273920.1273933
M. Hamana. Initial algebra semantics for cyclic sharing tree structures. Logical Methods in Computer Science, 6(3), 2010.
M. Hamana. Iteration algebras for UnQL graphs and completeness for bisimulation. In Proc. of Fixed Points in Computer Science (FICS'15), Electronic Proceedings in Theoretical Computer Science 191, pages 75-89, 2015.
M. Hamana, K. Matsuda, and K. Asada. The algebra of recursive graph transformation language UnCAL: Complete axiomatisation and iteration categorical semantics. submitted.
M. Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. PhD thesis, University of Edinburgh, 1997.
S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graph transformations. In Proc. of ICFP 2010, pages 205-216, 2010.
A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(3):447-468, 1996.
K. Matsuda and K. Asada. Graph transformation as graph reduction: A functional reformulation of graph-transformation language UnCAL. Technical Report GRACE-TR 2015-01, National Institute of Informatics, January 2015.
L. G. L. T. Meertens. Paramorphisms. Formal Asp. Comput., 4(5):413-424, 1992.
E. Meijer, M. M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proc of FPCA'91, pages 124-144, 1991.
R. Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984.
B. C.d.S. Oliveira and W. R. Cook. Functional programming with structured graphs. In Proc. of ICFP'12, pages 77-88, 2012.
A. K. Simpson and G. D. Plotkin. Complete axioms for categorical fixed-point operators. In Proc. of LICS'00, pages 30-41, 2000.
S. Staton. An algebraic presentation of predicate logic. In Proc. of FOSSACS 201, pages 401-417, 2013.
S. Staton. Algebraic effects, linearity, and quantum programming languages. In Proc. of POPL'15, pages 395-406, 2015.
G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Non-Omega-Overlapping TRSs are UN
This paper solves problem #79 of RTA's list of open
problems --- in the positive. If the rules of a TRS do not overlap w.r.t.
substitutions of infinite terms then the TRS has unique normal forms.
We solve the problem by reducing the problem to one of consistency for
"similar" constructor term rewriting systems. For this we introduce
a new proof technique. We define a relation ⇓ that is
consistent by construction, and which --- if transitive --- would
coincide with the rewrite system's equivalence relation =R.
We then prove the transitivity of ⇓ by coalgebraic
reasoning. Any concrete proof for instances of this relation only
refers to terms of some finite coalgebra, and we then construct an
equivalence relation on that coalgebra which coincides with ⇓.
consistency
omega-substitutions
uniqueness of normal forms
22:1-22:17
Regular Paper
Stefan
Kahrs
Stefan Kahrs
Connor
Smith
Connor Smith
10.4230/LIPIcs.FSCD.2016.22
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Complexity Hierarchies and Higher-Order Cons-Free Rewriting
Constructor rewriting systems are said to be cons-free if, roughly,
constructor terms in the right-hand sides of rules are subterms of
constructor terms in the left-hand side; the computational intuition
is that rules cannot build new data structures. It is well-known that
cons-free programming languages can be used to characterize
computational complexity classes, and that cons-free first-order term
rewriting can be used to characterize the set of polynomial-time
decidable sets.
We investigate cons-free higher-order term rewriting systems, the
complexity classes they characterize, and how these depend on the
order of the types used in the systems. We prove that, for every k >=
1, left-linear cons-free systems with type order k characterize
E^kTIME if arbitrary evaluation is used (i.e., the system does not
have a fixed reduction strategy).
The main difference with prior work in implicit complexity is that (i)
our results hold for non-orthogonal term rewriting systems with
possible rule overlaps with no assumptions about reduction strategy,
(ii) results for such term rewriting systems have previously only been
obtained for k = 1, and with additional syntactic restrictions on top
of cons-freeness and left-linearity.
Our results are apparently among the first implicit characterizations
of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior
results that having full non-determinism (via overlaps of rules) does
not directly allow for characterization of non-deterministic
complexity classes like NE. We also show that non-determinism makes
the classes characterized highly sensitive to minor syntactic changes
such as admitting product types or non-left-linear rules.
higher-order term rewriting
implicit complexity
cons-freeness
ETIME hierarchy
23:1-23:18
Regular Paper
Cynthia
Kop
Cynthia Kop
Jakob
Grue Simonsen
Jakob Grue Simonsen
10.4230/LIPIcs.FSCD.2016.23
M. Avanzini, N. Eguchi, and G. Moser. A new order-theoretic characterisation of the polytime computable functions. In APLAS, volume 7705 of LNCS, pages 280-295, 2012. URL: http://dx.doi.org/10.1007/978-3-642-35182-2_20.
http://dx.doi.org/10.1007/978-3-642-35182-2_20
M. Avanzini and G. Moser. Closing the gap between runtime complexity and polytime computability. In RTA, volume 6 of LIPIcs, pages 33-48, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.33.
http://dx.doi.org/10.4230/LIPIcs.RTA.2010.33
M. Avanzini and G. Moser. Polynomial path orders. LMCS, 9(4), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(4:9)2013.
http://dx.doi.org/10.2168/LMCS-9(4:9)2013
P. Baillot. From proof-nets to linear logic type systems for polynomial time computing. In TLCA, volume 4583 of LNCS, pages 2-7, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73228-0_2.
http://dx.doi.org/10.1007/978-3-540-73228-0_2
P. Baillot, M. Gaboardi, and V. Mogbil. A polytime functional language from light linear logic. In ESOP, volume 6012 of LNCS, pages 104-124, 2010. URL: http://dx.doi.org/10.1007/978-3-642-11957-6_7.
http://dx.doi.org/10.1007/978-3-642-11957-6_7
P. Baillot and U. Dal Lago. Higher-Order Interpretations and Program Complexity. In CSL, volume 16 of LIPIcs, pages 62-76, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2012.62.
http://dx.doi.org/10.4230/LIPIcs.CSL.2012.62
S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992. URL: http://dx.doi.org/10.1007/BF01201998.
http://dx.doi.org/10.1007/BF01201998
S. Bellantoni, K. Niggl, and H. Schwichtenberg. Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic, 104(1-3):17-30, 2000. URL: http://dx.doi.org/10.1016/S0168-0072(00)00006-3.
http://dx.doi.org/10.1016/S0168-0072(00)00006-3
F. Blanqui, J. Jouannaud, and A. Rubio. The computability path ordering: The end of a quest. In CSL, volume 5213 of LNCS, pages 1-14, 2008.
G. Bonfante. Some programming languages for logspace and ptime. In AMAST, volume 4019 of LNCS, pages 66-80, 2006. URL: http://dx.doi.org/10.1007/11784180_8.
http://dx.doi.org/10.1007/11784180_8
D. de Carvalho and J. Simonsen. An implicit characterization of the polynomial-time decidable sets by cons-free rewriting. In RTA-TLCA, volume 8560 of LNCS, pages 179-193, 2014.
M. Hofmann. Type systems for polynomial-time computation, 1999. Habilitationsschrift.
N. Jones. Computability and Complexity from a Programming Perspective. MIT Press, 1997.
N. Jones. The expressive power of higher-order types or, life without CONS. JFP, 11(1):55-94, 2001.
J. Jouannaud and A. Rubio. The higher-order recursive path ordering. In LICS, pages 402-411, 1999.
C. Kop and J. Simonsen. Complexity hierarchies and higher-order cons-free rewriting (extended version). Technical report, University of Copenhagen, 2016. Available online at the authors' homepages.
L. Kristiansen and K. Niggl. On the computational complexity of imperative programming languages. TCS, 318(1-2):139-161, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2003.10.016.
http://dx.doi.org/10.1016/j.tcs.2003.10.016
R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. TCS, 192(1):3-29, 1998.
C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
M. Sipser. Introduction to the Theory of Computation. Thomson Course Technology, 2006.
F. van Raamsdonk. Higher-order rewriting. In Term Rewriting Systems, Chapter 11. Cambridge University Press, 2003.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Weighted Relational Models for Mobility
We investigate operational and denotational semantics for
computational and concurrent systems with mobile names which capture
their computational properties. For example, various properties of
fixed networks, such as shortest or longest path, transition
probabilities, and secure data flows, correspond to the ``sum'' in a
semiring of the weights of paths through the network: we aim to model
networks with a dynamic topology in a similar way. Alongside rich
computational formalisms such as the lambda-calculus, these can be
represented as terms in a calculus of solos with weights from a
complete semiring $R$, so that reduction associates a weight in R to
each reduction path.
Taking inspiration from differential nets, we develop a denotational
semantics for this calculus in the category of sets and R-weighted
relations, based on its differential and compact-closed structure, but
giving a simple, syntax-independent representation of terms as
matrices over R. We show that this corresponds to the sum in R of
the values associated to its independent reduction paths, and that our
semantics is fully abstract with respect to the observational
equivalence induced by sum-of-paths evaluation.
Concurrency
Mobility
Denotational Semantics
24:1-24:15
Regular Paper
James
Laird
James Laird
10.4230/LIPIcs.FSCD.2016.24
A. Bahamonde. Tensor product of partially-additive monoids. Semigroup Forum, 32(1):31-53, 1985.
Emmanuel Beffara. Quantitative testing semantics for non-interleaving. CoRR, abs/0906.3994, 2009.
G. Bellin and P. J. Scott. On the pi-calculus and linear logic. Theoretical Computer Science, 135(1):11-65, 1994.
R. F. Blute, J. R. B. Cockett, and R. A. G. Seely. Differential categories. Mathematical. Structures in Comp. Sci., 16, 2006.
M. Boreale and F. Gaducci. Processes as formal power series: A coinductive approach to denotational semantics. Theoretical Computer Science, 360(1-3):440-458, 2006.
N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22:465-476, 1979.
T. Ehrhard and O. Laurent. Acyclic solos and differential interaction nets. Logical Methods in Computer Science, 6(3), 2010.
T. Ehrhard and O. Laurent. Interpreting a finitary pi-calculus in differential nets. Information and Computation, 208(6):606-633, 2010.
T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309, 2003.
T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006.
C. Fornet and G. Gonthier. The reflexive chemical abstract machine and the join-calculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL'96), 1996.
J. S. Golan. The theory of semirings with applications in mathematics and theoretical computer science. Addison-Wesley, 1992.
R. Guitart. Tenseurs et machines. Cahiers de Topologie et Geometrie Differentielle, XXI(1):5-62, 1980.
K. Honda and N. Yoshida. On reduction-based process semantics. Theoretical Computer Science, 152:437-686, 1995.
A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Math. Proc. Camb. Phil. Soc., 119:447-468, 1996.
J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. Weighted relational models of typed lambda-calculi. In Proceedings of LICS'13, 2013.
C. Laneve and B. Victor. Solos in concert. Mathematical Structures in Computer Science, 13(5), 2003.
P. Melliès, N. Tabareau, and C. Tasson. An explicit formula for the free exponential modality of linear logic. In Proc. ICALP'09, number 5556 in LNCS, pages 247-260, 2009.
R. Milner. Functions as processes. Math. Struct. in Computer Science, 2(2):119-141, 1992.
Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part i. I AND II. INFORMATION AND COMPUTATION, 100, 1989.
M. Mohri. Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics, 7(3):321-350, 2002.
C. Laneve. J. Parrow and B. Victor. Solo diagrams. In Proceedings of TACS 2001, LNCS. Springer, 2001.
J. Parrow and B. Victor. The fusion calculus: Expressiveness and symmetry in mobile processes. In Proceedings of LICS'98, pages 176-185. IEEE press, 1998.
D. Sangiorgi and D. Walker. The Pi-Calculus: A theory of mobile processes. Cambridge University Press, 2001.
L. Wischik and P. Gardner. Explicit fusions. Theoretical Computer Science, 340(3):606-630, 2005.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Focusing in Orthologic
We propose new sequent calculus systems for orthologic (also
known as minimal quantum logic) which satisfy the cut
elimination property. The first one is a very simple system relying on
the involutive status of negation. The second one incorporates the
notion of focusing (coming from linear logic) to add
constraints on proofs and thus to facilitate proof search. We
demonstrate how to take benefits from the new systems in automatic
proof search for orthologic.
orthologic
focusing
minimal quantum logic
linear logic
automatic proof search
cut elimination
25:1-25:17
Regular Paper
Olivier
Laurent
Olivier Laurent
10.4230/LIPIcs.FSCD.2016.25
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992.
Garrett Birkhoff. Lattice Theory, volume 25 of Colloquium Publications. American Mathematical Society, third edition, 1967.
Günter Bruns. Free ortholattices. Canadian Journal of Mathematics, 28(5):977-985, October 1976.
Uwe Egly and Hans Tompits. Gentzen-like methods in quantum logic. Technical Report 99-1, Institute for Programming and Logics, University at Albany - SUNY, 1999. Position Papers of TABLEAUX '99.
Uwe Egly and Hans Tompits. On different proof-search strategies for orthologic. Studia Logica, 73(1):131-152, February 2003.
Claudia Faggian and Giovanni Sambin. From basic logic to quantum logics with cut-elimination. International Journal of Theoretical Physics, 37(1):31-37, January 1998.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987.
Jean-Yves Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3):255-296, 1991.
Robert Goldblatt. Semantic analysis of orthologic. Journal of Philosophical Logic, 3(1-2):19-35, 1974.
Robert Goldblatt. Orthomodularity is not elementary. Journal of Symbolic Logic, 49(2):401-404, 1984.
Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, May 2004.
William McCune. Automatic proofs and counterexamples for some ortholattice identities. Information Processing Letters, 65(6):285-291, 1998.
Hirokazu Nishimura. Proof theory for minimal quantum logic I. International Journal of Theoretical Physics, 33(1):103-113, January 1994.
Jürgen Schulte Mönting. Cut elimination and word problems for varieties of lattices. Algebra Universalis, 12:290-321, December 1981.
Philip Whitman. Free lattices. Annals of Mathematics, 42(1):325-330, January 1941.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Functions-as-Constructors Higher-Order Unification
Unification is a central operation in the construction of a range of
computational logic systems based on first-order and higher-order
logics. First-order unification has a number of properties that
dominates the way it is incorporated within such systems. In
particular, first-order unification is decidable, unary, and can be
performed on untyped term structures. None of these three properties
hold for full higher-order unification: unification is undecidable,
unifiers can be incomparable, and term-level typing can dominate the
search for unifiers. The so-called pattern subset of
higher-order unification was designed to be a small extension to
first-order unification that respected the basic laws governing
lambda-binding (the equalities of alpha, beta, and
eta-conversion) but which also satisfied those three properties.
While the pattern fragment of higher-order unification has been
popular in various implemented systems and in various theoretical
considerations, it is too weak for a number of applications. In this
paper, we define an extension of pattern unification that is motivated
by some existing applications and which satisfies these three
properties. The main idea behind this extension is that the arguments
to a higher-order, free variable can be more than just distinct bound
variables: they can also be terms constructed from (sufficient numbers
of) such variables using term constructors and where no argument is a
subterm of any other argument. We show that this extension to pattern
unification satisfies the three properties mentioned above.
higher-order unification
pattern unification
26:1-26:17
Regular Paper
Tomer
Libal
Tomer Libal
Dale
Miller
Dale Miller
10.4230/LIPIcs.FSCD.2016.26
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Homological Computations for Term Rewriting Systems
An important problem in universal algebra consists in finding
presentations of algebraic theories by generators and relations, which
are as small as possible. Exhibiting lower bounds on the number of
those generators and relations for a given theory is a difficult task
because it a priori requires considering all possible sets of
generators for a theory and no general method exists. In this article,
we explain how homological computations can provide such lower bounds,
in a systematic way, and show how to actually compute those in the
case where a presentation of the theory by a convergent rewriting
system is known. We also introduce the notion of coherent presentation
of a theory in order to consider finer homotopical invariants. In some
aspects, this work generalizes, to term rewriting systems, Squier's
celebrated homological and homotopical invariants for string rewriting
systems.
term rewriting system
Lawvere theory
Tietze equivalence
resolution
homology
convergent pres entation
coherent presentation
27:1-27:17
Regular Paper
Philippe
Malbos
Philippe Malbos
Samuel
Mimram
Samuel Mimram
10.4230/LIPIcs.FSCD.2016.27
Jiří Adámek and Jiří Rosicky. Locally presentable and accessible categories, volume 189. Cambridge University Press, 1994.
Michael Barr. Cartan-Eilenberg cohomology and triples. Journal of Pure and Applied Algebra, 112(3):219-238, 1996.
Jonathan Mock Beck. Triples, algebras and cohomology. PhD thesis, Columbia Univ, 1967.
Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical computer science, 115(1):43-62, 1993.
Yves Guiraud, Philippe Malbos, and Samuel Mimram. A homotopical completion procedure with applications to coherence of monoids. In RTA, volume 21, pages 223-238. Dagstuhl, 2013.
Allen Hatcher. Algebraic Topology. Cambridge University Press, 2002.
Graham Higman and B. H. Neumann. Groups as groupoids with one law. Publicationes Mathematicae Debrecen, 2(215-227):228, 1952.
Mamuka Jibladze and Teimuraz Pirashvili. Cohomology of algebraic theories. Journal of Algebra, 137(2):253-296, 1991.
Mamuka Jibladze and Teimuraz Pirashvili. Quillen cohomology and Baues-Wirsching cohomology of algebraic theories. Cahiers de top. et géom. diff. cat., 47(3):163-205, 2006.
Donald E Knuth and Peter B Bendix. Simple word problems in universal algebras. In Automation of Reasoning, pages 342-376. Springer, 1983.
Yuji Kobayashi. Complete rewriting systems and homology of monoid algebras. Journal of Pure and Applied Algebra, 65(3):263-275, 1990.
Yves Lafont and Alain Prouté. Church-rooser property and homology of monoids. Mathematical Structures in Computer Science, 1(03):297-326, 1991.
F William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(5):869, 1963.
Jean-Louis Loday and Bruno Vallette. Algebraic operads, volume 346 of Grundlehren der Mathematischen Wissenschaften. Springer, Heidelberg, 2012.
Saunders Mac Lane. Homology. Springer-Verlag, Berlin, 1995.
Philippe Malbos. Critères de finitude homologique pour la non convergence des systèmes de réécriture de termes. PhD thesis, Université de Montpellier II, 2004.
William Mccune et al. Single Axioms: With and Without Computers. In Computer Mathematics: Proceedings of the Fourth Asian Symposium (ASCM 2000), page 83. World Scientific, 2000.
William McCune, Ranganathan Padmanabhan, and Robert Veroff. Yet another single law for lattices. Algebra Universalis, 50(2):165-169, 2003.
William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, and Larry Wos. Short single axioms for Boolean algebra. Journal of Automated Reasoning, 29(1):1-16, 2002.
Ralph McKenzie. Equational Bases for Lattice Theories. Math. Scandinavica, 27:24-38, 1970.
Paul-André Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In Rewriting techniques and applications, pages 24-50. Springer, 2002.
Barry Mitchell. Rings with several objects. Advances in Mathematics, 8(1):1-161, 1972.
B. H. Neumann et al. Yet another single law for groups. Illinois Journal of Mathematics, 30(2):295-300, 1986.
Bernhard Hermann Neumann. Another single law for groups. Bulletin of the Australian Mathematical Society, 23(01):81-102, 1981.
Maxwell Herman Alexander Newman. On theories with a combinatorial definition of "equivalence". Annals of mathematics, pages 223-243, 1942.
R Padmanabhan and RW Quackenbush. Equational theories of algebras with distributive congruences. Proceedings of the American Mathematical Society, 41(2):373-377, 1973.
DH Potts. Axioms for semi-lattices. Canad. Math Bulletin, 8:519, 1965.
Craig Squier and Friedrich Otto. The word problem for finitely presented monoids and finite canonical rewriting systems. In Rewriting Techniques and Applications, pages 74-82. Springer, 1987.
Craig C Squier, Friedrich Otto, and Yuji Kobayashi. A finiteness condition for rewriting systems. Theoretical Computer Science, 131(2):271-294, 1994.
Alfred Tarski. Ein Beitrag zur Axiomatik der Abelschen Gruppen. Fundamenta Mathematicae, 1(30):253-256, 1938.
Heinrich Tietze. Über die topologischen Invarianten mehrdimensionaler Mannigfaltigkeiten. Monatsh. Math. Phys., 19(1):1-118, 1908.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Reversible Term Rewriting
Essentially, in a reversible programming language, for each forward
computation step from state S to state S', there exists a
constructive and deterministic method to go backwards from state S'
to state S. Besides its theoretical interest, reversible
computation is a fundamental concept which is relevant in many
different areas like cellular automata, bidirectional program
transformation, or quantum computing, to name a few. In this paper,
we focus on term rewriting, a computation model that underlies most
rule-based programming languages. In general, term rewriting is not
reversible, even for injective functions; namely, given a rewrite step
t1 -> t2, we do not always have a decidable and deterministic
method to get t1 from t2. Here, we introduce a conservative
extension of term rewriting that becomes reversible. Furthermore, we
also define a transformation to make a rewrite system reversible using
standard term rewriting.
term rewriting
reversible computation
program transformation
28:1-28:18
Regular Paper
Naoki
Nishida
Naoki Nishida
Adrián
Palacios
Adrián Palacios
Germán
Vidal
Germán Vidal
10.4230/LIPIcs.FSCD.2016.28
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
Suzuki et al. showed that properly oriented, right-stable, orthogonal, and oriented conditional term rewrite systems with extra variables in right-hand sides are confluent. We present our Isabelle/HOL formalization of this result, including two generalizations. On the one hand, we relax proper orientedness and orthogonality to extended proper orientedness and almost orthogonality modulo infeasibility, as suggested by Suzuki et al. On the other hand, we further loosen the requirements of the latter, enabling more powerful methods for proving infeasibility of conditional critical pairs. Furthermore, we formalized a construction by Jacquemard that employs exact tree automata completion for non-reachability analysis and apply it to certify infeasibility of conditional critical pairs. Combining these two results and extending the conditional confluence checker ConCon accordingly, we are able to automatically prove and certify confluence of an important class of conditional term rewrite systems.
certification
conditional term rewriting
confluence
infeasible critical pairs
non-reachability
29:1-29:16
Regular Paper
Christian
Sternagel
Christian Sternagel
Thomas
Sternagel
Thomas Sternagel
10.4230/LIPIcs.FSCD.2016.29
Jürgen Avenhaus and Carlos Loría-Sáenz. On conditional rewrite systems with extra variables and deterministic logic programs. In Proceedings of the 5th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 822 of Lecture Notes in Computer Science, pages 215-229. Springer, 1994. \doi10.1007/3-540-58216-9_40.
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
Bertram Felgenhauer and René Thiemann. Reachability analysis with state-compatible automata. In Proceedings of the 8th International Conference on Language and Automata Theory and Applications, volume 8370 of Lecture Notes in Computer Science, pages 347-359. Springer, 2014. \doi10.1007/978-3-319-04921-2_28.
Thomas Genet. Decidable approximations of sets of descendants and sets of normal forms. In Proceedings of the 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer, 1998. \doi10.1007/BFb0052368.
Thomas Genet and Valerié Viet Triem Tong. Reachability analysis of term rewriting systems with timbuk. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 2250 of Lecture Notes in Computer Science, pages 695-706. Springer, 2001. \doi10.1007/3-540-45653-8_48.
Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. Proving and disproving termination of higher-order functions. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems, volume 3717 of Lecture Notes in Computer Science, pages 216-231. Springer, 2005. \doi10.1007/11559306_12.
Michael Hanus. On extra variables in (equational) logic programming. In Proceedings of the 12th International Conference on Logic Programming, pages 665-679. MIT Press, 1995.
Florent Jacquemard. Decidable approximations of term rewriting systems. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 362-376. Springer, 1996. \doi10.1007/3-540-61464-8_65.
Tobias Nipkow, Lawrence Charles Paulson, and Makarius Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. \doi10.1007/3-540-45949-9.
Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002.
Christian Sternagel and Aart Middeldorp. Root-labeling. In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 336-350. Springer, 2008. \doi10.1007/978-3-540-70590-1_23.
Christian Sternagel and Thomas Sternagel. Level-confluence of 3-CTRSs in Isabelle/HOL. In Tiwari and Aoto [18]. URL: http://www.csl.sri.com/users/tiwari/iwc2015/iwc2015.pdf.
http://www.csl.sri.com/users/tiwari/iwc2015/iwc2015.pdf
Christian Sternagel and René Thiemann. Signature extensions preserve termination - an alternative proof via dependency pairs. In Proceedings of the 19h EACSL Annual Conference on Computer Science Logic, volume 6247 of Lecture Notes in Computer Science, pages 514-528. Springer, 2010. \doi10.1007/978-3-642-15205-4_39.
Christian Sternagel and René Thiemann. The Certification Problem Format. In Proceedings of the 11th Workshop on User Interfaces for Theorem Provers, pages 61-72, 2014. \doi10.4204/EPTCS.167.8.
Thomas Sternagel and Aart Middeldorp. Conditional confluence (system description). In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science, pages 456-465. Springer, 2014. \doi10.1007/978-3-319-08918-8_31.
Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 179-193. Springer, 1995. \doi10.1007/3-540-59200-8_56.
René Thiemann and Christian Sternagel. Certification of termination proofs using Cęrn-0.2exeęrn-0.5exTęrn-0.5exA. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 452-468. Springer, 2009. \doi10.1007/978-3-642-03359-9_31.
Ashish Tiwari and Takahito Aoto, editors. Proceedings of the 4th International Workshop on Confluence, 2015. URL: http://www.csl.sri.com/users/tiwari/iwc2015/iwc2015.pdf.
http://www.csl.sri.com/users/tiwari/iwc2015/iwc2015.pdf
Makarius Wenzel. System description: Isabelle/jEdit in 2014. In Proceedings of the 11th Workshop on User Interfaces for Theorem Provers, pages 84-94, 2014. \doi10.4204/EPTCS.167.10.
Sarah Winkler and René Thiemann. Formalizing soundness and completeness of unravelings. In Proceedings of the 10th International Workshop on Frontiers of Combining Systems, volume 9322 of Lecture Notes in Computer Science, pages 239-255. Springer, 2015. \doi10.1007/978-3-319-24246-0_15.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Category Theory in Coq 8.5
We report on our experience implementing category theory in Coq 8.5.
Our work formalizes most of basic category theory, including concepts
not covered by existing formalizations, in a library that is fit to be
used as a general-purpose category-theoretical foundation.
Our development particularly takes advantage of two features new to
Coq 8.5: primitive projections for records and universe polymorphism.
Primitive projections allow for well-behaved dualities while universe
polymorphism provides a relative notion of largeness and smallness.
The latter is one of the main contributions of this paper. It pushes
the limits of the new universe polymorphism and constraint inference
algorithm of Coq 8.5.
In this paper we present in detail smallness and largeness in
categories and the foundation they are built on top of. We
furthermore explain how we have used the universe polymorphism of Coq 8.5
to represent smallness and largeness arguments by simply ignoring
them and entrusting them to the universe inference algorithm of Coq 8.5.
We also briefly discuss our experience throughout this
implementation, discuss concepts formalized in this development and
give a comparison with a few other developments of similar extent.
Category Theory
Coq 8.5
Universe Polymorphism
Homotopy Type Theory
30:1-30:18
Regular Paper
Amin
Timany
Amin Timany
Bart
Jacobs
Bart Jacobs
10.4230/LIPIcs.FSCD.2016.30
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the rezk completion. Mathematical Structures in Computer Science, 25(05):1010-1039, jan 2015. URL: https://github.com/benediktahrens/rezk_completion, URL: http://dx.doi.org/10.1017/s0960129514000486.
http://dx.doi.org/10.1017/s0960129514000486
Steve Awodey. Category theory. Oxford University Press, 2010.
Bodil Biering, Lars Birkedal, and Noah Torp-Smith. Bi-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst., 29(5), August 2007. URL: http://dx.doi.org/10.1145/1275497.1275499.
http://dx.doi.org/10.1145/1275497.1275499
Lars Birkedal, Rasmus Ejlers Mogelberg, Jan Schwinghammer, and Kristian Stovring. First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. Institute of Electrical & Electronics Engineers (IEEE), jun 2011. URL: http://dx.doi.org/10.1109/lics.2011.16.
http://dx.doi.org/10.1109/lics.2011.16
Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. The category-theoretic solution of recursive metric-space equations. Theoretical Computer Science, 411(47):4102-4122, oct 2010. URL: http://dx.doi.org/10.1016/j.tcs.2010.07.010.
http://dx.doi.org/10.1016/j.tcs.2010.07.010
T. Coquand. An analysis of Girard’s paradox. Technical Report RR-0531, INRIA, May 1986. URL: https://hal.inria.fr/inria-00076023.
https://hal.inria.fr/inria-00076023
Jason Gross, Adam Chlipala, and David I. Spivak. Experience Implementing a Performant Category-Theory Library in Coq. In Interactive Theorem Proving - 5th International Conference, ITP 2014. Proceedings, pages 275-291, July 2014. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_18.
http://dx.doi.org/10.1007/978-3-319-08970-6_18
Jason Gross, Adam Chlipala, and David I. Spivak. Experience implementing a performant category-theory library in coq, 2014. URL: http://arxiv.org/abs/arXiv:1401.7694.
http://arxiv.org/abs/arXiv:1401.7694
Gérard P. Huet and Amokrane Saïbi. Constructive category theory. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 239-276, 2000. URL: http://www.lix.polytechnique.fr/coq/pylons/coq/pylons/contribs/view/ConCaT/v8.4.
http://www.lix.polytechnique.fr/coq/pylons/coq/pylons/contribs/view/ConCaT/v8.4
Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999.
Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science &Business Media, 1978.
The Coq development team. Coq 8.5 Reference Manual. Inria, 2015.
Colin McLarty. Elementary Categories, Elementary Toposes. Oxford University Press, Oxford, UK, 1996.
Adam Megacz. Category Theory in Coq. URL: http://www.megacz.com/berkeley/coq-categories/.
http://www.megacz.com/berkeley/coq-categories/
John C. Mitchell. Foundations of Programming Languages. MIT Press, Cambridge, MA, USA, 1996.
Daniel Peebles, James Deikun, Ulf Norell, Dan Doel, Andrea Vezzosi, Darius Jahandarie, and James Cook. copumpkin/categories. URL: https://github.com/copumpkin/categories.
https://github.com/copumpkin/categories
Antonino Salibra. Scott is always simple. In Proceedings of the 37th International Conference on Mathematical Foundations of Computer Science, MFCS'12, pages 31-45, Berlin, Heidelberg, 2012. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-32589-2_3.
http://dx.doi.org/10.1007/978-3-642-32589-2_3
Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq. In Interactive Theorem Proving, ITP 2014, Proceedings, pages 499-514, July 2014. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_32.
http://dx.doi.org/10.1007/978-3-319-08970-6_32
The Univalent Foundations Program. HoTT Version of Coq and Library. URL: https://github.com/HoTT/HoTT.
https://github.com/HoTT/HoTT
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
http://homotopytypetheory.org/book
Amin Timany. Categories. URL: https://github.com/amintimany/Categories/tree/FSCD16, URL: http://dx.doi.org/10.5281/zenodo.50689.
http://dx.doi.org/10.5281/zenodo.50689
Amin Timany. Categories-HoTT. URL: https://github.com/amintimany/Categories-HoTT.
https://github.com/amintimany/Categories-HoTT
Amin Timany and Bart Jacobs. The Category-theoretic Solution of Recursive Ultra-metric Space Equations. Presented at CoqPL'16: The Second International Workshop on Coq for PL. URL: https://github.com/amintimany/CTDT.
https://github.com/amintimany/CTDT
Amin Timany and Bart Jacobs. First Steps Towards Cumulative Inductive Types in CIC. In 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015) 2015. Proceedings, pages 608-617, 2015. URL: http://dx.doi.org/10.1007/978-3-319-25150-9_36.
http://dx.doi.org/10.1007/978-3-319-25150-9_36
Amin Timany and Bart Jacobs. Category Theory in Coq 8.5: Extended Version. Technical Report CW697, iMinds-Distrinet, KU Leuven, April 2016. URL: http://www2.cs.kuleuven.be/publicaties/rapporten/cw/CW697.abs.html.
http://www2.cs.kuleuven.be/publicaties/rapporten/cw/CW697.abs.html
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Formal Languages, Formally and Coinductively
Traditionally, formal languages are defined as sets of words. More
recently, the alternative coalgebraic or coinductive representation as
infinite tries, i.e., prefix trees branching over the alphabet, has
been used to obtain compact and elegant proofs of classic results in
language theory. In this paper, we study this representation in the
Isabelle proof assistant. We define regular operations on infinite
tries and prove the axioms of Kleene algebra for those
operations. Thereby, we exercise corecursion and coinduction and
confirm the coinductive view being profitable in formalizations, as it
improves over the set-of-words view with respect to proof automation.
Formal languages
codatatypes
corecursion
coinduction
interactive theorem proving
Isabelle HOL
31:1-31:17
Regular Paper
Dmitriy
Traytel
Dmitriy Traytel
10.4230/LIPIcs.FSCD.2016.31
Andreas Abel and Brigitte Pientka. Wellfounded recursion with copatterns: A unified approach to termination and productivity. In G. Morrisett and T. Uustalu, editors, ICFP'13, pages 185-196. ACM, 2013.
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In R. Giacobazzi and R. Cousot, editors, POPL'13, pages 27-38. ACM, 2013.
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014.
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Foundational extensible corecursion. In J. Reppy, editor, ICFP 2015, pages 192-204. ACM, 2015.
Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, and Alexandra Silva. Brzozowski’s algorithm (co)algebraically. In R.L. Constable and A. Silva, editors, Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, volume 7230 of LNCS, pages 12-23. Springer, 2012.
Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In R. Giacobazzi and R. Cousot, editors, POPL'13, pages 457-468. ACM, 2013.
Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: http://dx.doi.org/10.1145/321239.321249.
http://dx.doi.org/10.1145/321239.321249
Adam Chlipala. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. URL: http://mitpress.mit.edu/books/certified-programming-dependent-types.
http://mitpress.mit.edu/books/certified-programming-dependent-types
Eduardo Giménez and Pierre Castéran. A tutorial on [co-]inductive types in Coq. 1998. URL: http://www.labri.fr/perso/casteran/RecTutorial.pdf.
http://www.labri.fr/perso/casteran/RecTutorial.pdf
Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, FLOPS 2010, volume 6009 of LNCS, pages 103-117. Springer, 2010.
Ralf Hinze. Concrete stream calculus: An extended study. J. Funct. Program., 20(5-6):463-535, 2010.
Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222-259, 1997.
Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput., 110(2):366-390, 1994.
Dexter Kozen and Alexandra Silva. Practical coinduction. Technical report, Cornell University, 2012. URL: http://hdl.handle.net/1813/30510.
http://hdl.handle.net/1813/30510
Alexander Krauss and Tobias Nipkow. Proof pearl: Regular expression equivalence and relation algebra. J. Automated Reasoning, 49:95-106, 2012. published online March 2011.
Andreas Lochbihler and Johannes Hölzl. Recursive functions on lazy lists via domains and topologies. In G. Klein and R. Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 341-357. Springer, 2014.
Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer, 2014. URL: http://www.in.tum.de/~nipkow/Concrete-Semantics.
http://www.in.tum.de/~nipkow/Concrete-Semantics
Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. J. Logic Comp., 7(2):175-204, 1997.
Lawrence C. Paulson. A formalisation of finite automata using hereditarily finite sets. In A.P. Felty and A. Middeldorp, editors, CADE-25, volume 9195 of LNCS, pages 231-245. Springer, 2015.
Tillmann Rendel, Julia Trieflinger, and Klaus Ostermann. Automatic refunctionalization to a language with copattern matching: with applications to the expression problem. In K. Fisher and J.H. Reppy, editors, ICFP 2015, pages 269-279. ACM, 2015.
Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coinductive proof techniques for language equivalence. In A. Horia Dediu, C. Martín-Vide, and B. Truthe, editors, LATA 2013, volume 7810 of LNCS, pages 480-492. Springer, 2013.
Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Proving language inclusion and equivalence by coinduction. Inf. Comput., 246:62-76, 2016.
J. J. M. M. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000.
Jan J. M. M. Rutten. Automata and coinduction (an exercise in coalgebra). In D. Sangiorgi and R. de Simone, editors, CONCUR 1998, volume 1466 of LNCS, pages 194-218. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0055624.
http://dx.doi.org/10.1007/BFb0055624
Anton Setzer. How to reason coinductively informally. To appear in R. Kahle, T. Strahm, and T. Studer (Eds.): Festschrift on occasion of Gerhard Jäger’s 60th birthday. Available from http://www.cs.swan.ac.uk/~csetzer/articles/jaeger60Birthdaymain.pdf, 2015.
http://www.cs.swan.ac.uk/~csetzer/articles/jaeger60Birthdaymain.pdf
Alexandra Silva. A short introduction to the coalgebraic method. ACM SIGLOG News, 2(2):16-27, 2015.
Dmitriy Traytel. A codatatype of formal languages. In Archive of Formal Proofs. 2013. URL: http://afp.sf.net/entries/Coinductive_Languages.shtml.
http://afp.sf.net/entries/Coinductive_Languages.shtml
Dmitriy Traytel. A coalgebraic decision procedure for WS1S. In Stephan Kreutzer, editor, CSL 2015, volume 41 of LIPIcs, pages 487-503. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compositional (co)datatypes for higher-order logic - Category theory applied to theorem proving. In LICS 2012, pages 596-605. IEEE Computer Society, 2012.
Dmytro Traytel. Formalizing Symbolic Decision Procedures for Regular Languages. PhD thesis, TU München, 2015. URL: http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20151016-1273011-1-9.
http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20151016-1273011-1-9
Philip Wadler. The Expression Problem. Available online at: http://tinyurl.com/wadler-ep, 1998.
http://tinyurl.com/wadler-ep
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Normalisation by Random Descent
We present abstract hyper-normalisation results for strategies. These
results are then applied to term rewriting systems, both first and
higher-order. For example, we show hyper-normalisation of the
left--outer strategy for, what we call, left--outer pattern rewrite
systems, a class comprising both Combinatory Logic and the
lambda-calculus but also systems with critical pairs. Our
results apply to strategies that need not be deterministic but do have
Newman's random descent property: all reductions to normal form have
the same length, with Huet and Lévy's external strategy being an
example. Technically, we base our development on supplementing the
usual notion of commutation diagram with a notion of order, expressing
that the measure of its right leg does not exceed that of its left
leg, where measure is an abstraction of the usual notion of length.
We give an exact characterisation of such global commutation diagrams,
for pairs of reductions, by means of local ones, for pairs of steps,
we dub Dyck diagrams.
strategy
hyper-normalisation
commutation
random descent
32:1-32:18
Regular Paper
Vincent
van Oostrom
Vincent van Oostrom
Yoshihito
Toyama
Yoshihito Toyama
10.4230/LIPIcs.FSCD.2016.32
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2nd revised edition, 1984.
H.P. Barendregt, J.R.K. Kennaway, J.W. Klop, and M.R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information &Computation, 75(3):191-231, 1987. URL: http://dx.doi.org/10.1016/0890-5401(87)90001-0.
http://dx.doi.org/10.1016/0890-5401(87)90001-0
N. Dershowitz. On lazy commutation. In Languages: From Formal to Natural, volume 5533 of Lecture Notes in Computer Science, pages 59-82. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-01748-3_5.
http://dx.doi.org/10.1007/978-3-642-01748-3_5
J.R.W. Glauert, R. Kennaway, and Z. Khasidashvili. Stable results and relative normalization. Journal of Logic and Computation, 10(3):323-348, 2000. URL: http://dx.doi.org/10.1093/logcom/10.3.323.
http://dx.doi.org/10.1093/logcom/10.3.323
M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 138-152. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61464-8_48.
http://dx.doi.org/10.1007/3-540-61464-8_48
N. Hirokawa, A. Middeldorp, and G. Moser. Leftmost outermost revisited. In Proceedings of the 26th International Conference on Rewriting Techniques and Applications, volume 36 of Leibniz International Proceedings in Informatics, pages 209-222, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2015.209.
http://dx.doi.org/10.4230/LIPIcs.RTA.2015.209
Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, \setcounterRomancnt1\RomanRomancnt. In Computational Logic: Essays in Honor of Alan Robinson. The MIT Press, 1991. (accessed 27-4-2016). URL: http://pauillac.inria.fr/~levy/pubs/81robinson1.pdf.
http://pauillac.inria.fr/~levy/pubs/81robinson1.pdf
J.W. Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht, 1980. (accessed 27-4-2016). URL: http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/9.PhDthesis-total.pdf.
http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/9.PhDthesis-total.pdf
R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3-29, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(97)00143-6.
http://dx.doi.org/10.1016/S0304-3975(97)00143-6
P.-A. Melliès. A stability theorem in rewriting theory. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 287-298. IEEE Computer Society Press, 1998. URL: http://dx.doi.org/10.1109/LICS.1998.705665.
http://dx.doi.org/10.1109/LICS.1998.705665
D. Miller. Unification of simply typed lambda-terms as logic programming. In Proceedings of the 8th International Conference on Logic Programming, pages 253-281. The MIT Press, 1991. (accessed 27-4-2016). URL: http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp91.pdf.
http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp91.pdf
M. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43(2):223-243, 1942. URL: http://dx.doi.org/10.2307/1968867.
http://dx.doi.org/10.2307/1968867
M.J. O'Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer, 1977. URL: http://dx.doi.org/10.1007/3-540-08531-9.
http://dx.doi.org/10.1007/3-540-08531-9
V. van Oostrom. Finite family developments. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 308-322. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-62950-5_80.
http://dx.doi.org/10.1007/3-540-62950-5_80
V. van Oostrom. Random descent. In Proceedings of the 18th International Conference on Rewriting Techniques and Applications, volume 4533 of Lecture Notes in Computer Science, pages 314-328. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73449-9_24.
http://dx.doi.org/10.1007/978-3-540-73449-9_24
V. van Oostrom. Confluence by decreasing diagrams - converted. In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 306-320. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70590-1_21.
http://dx.doi.org/10.1007/978-3-540-70590-1_21
R.C. Sekar and I.V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 230-241. IEEE Computer Society Press, 1990. URL: http://dx.doi.org/10.1109/LICS.1990.113749.
http://dx.doi.org/10.1109/LICS.1990.113749
Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
Y. Toyama. Strong sequentiality of left-linear overlapping term rewriting systems. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, pages 274-284. IEEE Computer Society Press, 1992. URL: http://dx.doi.org/10.1109/LICS.1992.185540.
http://dx.doi.org/10.1109/LICS.1992.185540
Y. Toyama. Reduction strategies for left-linear term rewriting systems. In Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 198-223. Springer, 2005. URL: http://dx.doi.org/10.1007/11601548_13.
http://dx.doi.org/10.1007/11601548_13
F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In Proceedings of the Colloquium on Algebra, Combinatorics and Logic in Computer Science, Volume \setcounterRomancnt2\RomanRomancnt, volume 42 of Colloquia Mathematica Societatis J. Bolyai, pages 849-869, 1986.
D.A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993.
H. Zantema, B. König, and H.J.S. Bruggink. Termination of cycle rewriting. In Proceedings of the 25th International Conference on Rewriting Techniques and Applicationsand the 12th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, pages 476-490. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08918-8_33.
http://dx.doi.org/10.1007/978-3-319-08918-8_33
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Ground Confluence Prover based on Rewriting Induction
Ground confluence of term rewriting systems guarantees that all ground
terms are confluent. Recently, interests in proving confluence of
term rewriting systems automatically has grown, and confluence provers
have been developed. But they mainly focus on confluence and not
ground confluence. In fact, little interest has been paid to
developing tools for proving ground confluence automatically. We
report an implementation of a ground confluence prover based on
rewriting induction, which is a method originally developed for
proving inductive theorems.
Ground Confluence
Rewriting Induction
Non-Orientable Equations
Term Rewriting Systems
33:1-33:12
Regular Paper
Takahito
Aoto
Takahito Aoto
Yoshihito
Toyama
Yoshihito Toyama
10.4230/LIPIcs.FSCD.2016.33
T. Aoto. Dealing with non-orientable equations in rewriting induction. In Proc. of 17th RTA, volume 4098 of LNCS, pages 242-256. Springer-Verlag, 2006.
T. Aoto. Designing a rewriting induction prover with an increased capability of non-orientable equations. In Proc. of 1st SCSS, RISC Technical Report, pages 1-15, 2008.
T. Aoto. Sound lemma generation for proving inductive validity of equations. In Proc. of 28th FSTTCS, volume 2 of LIPIcs, pages 13-24. Schloss Dagstuhl, 2008.
T. Aoto and S. Stratulat. Decision procedures for proving inductive theorems without induction. In Proc. of 16th PPDP, pages 237-248. ACM Press, 2014.
T. Aoto and Y. Toyama. Persistency of confluence. Journal of Universal Computer Science, 3(11):1134-1147, 1997.
T. Aoto, Y. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In Proc. of 20th RTA, volume 5595 of LNCS, pages 93-102. Springer-Verlag, 2009.
K. Becker. Proving ground confluence and inductive validity in constructor based equational specifications. In Proc. of 4th TAPSOFT, volume 668 of LNCS, pages 46-60. Springer-Verlag, 1993.
A. Bouhoula. Simultaneous checking of completeness and ground conflunce for algebraic specifications. ACM Transactions on Computational Logic, 10(2):20:1-33, 2009.
A. Bouhoula and F. Jacquemard. Verifying regular trace properties of secuirty protocols with explicit destructors and implicit induction. In Proc. of FCS-ARSPA, pages 27-44, 2007.
A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631-668, 1995.
Y. Chiba, T. Aoto, and Y. Toyama. Program transformation by templates based on term rewriting. In Proc. of 7th PPDP, pages 59-69. ACM Press, 2005.
M. Codish, V. Lagoon, and P. J. Stuckey. Solving partial order constraints for LPO termination. In Proc. of 17th RTA, volume 4098 of LNCS, pages 4-18. Springer-Verlag, 2006.
N. Dershowitz and U. S. Reddy. Deductive and inductive synthesis of equational programs. Journal of Symbolic Computation, 15:467-494, 1993.
L. Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253-276, 1989.
H. Ganzinger. Ground term confluence in parametric conditional equational specifications. In Proc. of 4th STACS, volume 247 of LNCS, pages 286-298, 1987.
R. Göbel. Ground confluence. In Proc. of 2nd RTA, volume 256 of LNCS, pages 156-167, 1987.
N. Hirokawa and D. Klein. Saigawa: A confluence tool. In Proc. of 1st IWC, page 49, 2012.
D. Kapur, P. Narendran, and F. Otto. On ground-confluence of term rewriting systems. Information and Computation, 86:14-31, 1990.
D. Kapur, P. Narendran, and H. Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395-415, 1987.
D. Kapur, P. Narendran, and H. Zhang. Automating inductionless induction using test sets. Journal of Symbolic Computation, 11(1-2):81-111, 1991.
K. Sato, K. Kikuchi, T. Aoto, and Y. Toyama. Correctness of context-moving transformations for term rewriting systems. In Proc. of 25th LOPSTR, volume 9527 of LNCS, pages 331-345. Springer-Verlag, 2015.
S. Shimazu, T. Aoto, and Y. Toyama. Automated lemma generation for rewriting induction with disproof. JSSST Computer Software, 26(2):41-55, 2009. In Japanese.
T. Sternagel and A. Middeldorp. Conditional confluence (system description). In Proc. of Joint 25th RTA and 12th TLCA, pages 456-465. Springer-Verlag, 2014.
Terese. Term Rewriting Systems. Cambridge University Press, 2003.
T. Walsh. A divergence critic for inductive proof. Journal of Artificial Intelligence Research, 4:209-235, 1996.
F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In Proc. of the Colloq. on Algebra, Combinatorics and Logic in Computer Science, Vol. II, pages 849-869. Springer-Verlag, 1985.
H. Zankl, B. Felgenhauer, and A. Middeldorp. CSI - A confluence tool. In Proc. of 23rd CADE, volume 6803 of LNAI, pages 499-505. Springer-Verlag, 2011.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Globular: An Online Proof Assistant for Higher-Dimensional Rewriting
This article introduces Globular, an online proof assistant for the
formalization and verification of proofs in higher-dimensional
category theory. The tool produces graphical visualizations of
higher-dimensional proofs, assists in their construction with a
point-and-click interface, and performs type checking to prevent
incorrect rewrites. Hosted on the web, it has a low barrier to use,
and allows hyperlinking of formalized proofs directly from research
papers. It allows the formalization of proofs from logic, topology and
algebra which are not formalizable by other methods, and we give
several examples.
higher category theory
higher-dimensional rewriting
interactive theorem proving
34:1-34:11
Regular Paper
Krzysztof
Bar
Krzysztof Bar
Aleks
Kissinger
Aleks Kissinger
Jamie
Vicary
Jamie Vicary
10.4230/LIPIcs.FSCD.2016.34
John C. Baez and Aaron D. Lauda. Higher-dimensional algebra V: 2-groups. Theory and Applications of Categories, 12:423-491, 2004. URL: http://www.tac.mta.ca/tac/volumes/12/14/12-14abs.html.
http://www.tac.mta.ca/tac/volumes/12/14/12-14abs.html
John W. Barrett, Catherine Meusburger, and Gregor Schaumann. Gray categories with duals and their diagrams. J. Diff. Geom., to appear. URL: http://arxiv.org/abs/1211.0529.
http://arxiv.org/abs/1211.0529
Eric Finster. The Orchard proof assistant. URL: https://github.com/ericfinster/orchard.
https://github.com/ericfinster/orchard
Yves Guiraud. Polygraphs for termination of left-linear term rewriting systems. 2007. URL: http://arxiv.org/abs/cs/0702040.
http://arxiv.org/abs/cs/0702040
HoTT Formalisations in Coq and Agda. URL: http://homotopytypetheory.org/coq.
http://homotopytypetheory.org/coq
André Joyal and Ross Street. The geometry of tensor calculus, I. Adv. Math., 88(1):55-112, 1991. URL: http://dx.doi.org/10.1016/0001-8708(91)90003-p.
http://dx.doi.org/10.1016/0001-8708(91)90003-p
Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In CADE-25 - 25th International Conference on Automated Deduction, volume 9195 of LNCS. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21401-6_22.
http://dx.doi.org/10.1007/978-3-319-21401-6_22
Joachim Kock. Frobenius Algebras and 2D Topological Quantum Field Theories. Cambridge University Press (CUP), 2003. URL: http://dx.doi.org/10.1017/cbo9780511615443.
http://dx.doi.org/10.1017/cbo9780511615443
Stephen Lack. A coherent approach to pseudomonads. Adv. Math., 152(2):179-202, 2000. URL: http://dx.doi.org/10.1006/aima.1999.1881.
http://dx.doi.org/10.1006/aima.1999.1881
Yves Lafont. Algebra and geometry of rewriting. Applied Categorical Structures, 15(4):415-437, 2007. URL: http://dx.doi.org/10.1007/s10485-007-9083-6.
http://dx.doi.org/10.1007/s10485-007-9083-6
Tom Leinster. A survey of definitions of n-category. Theory and Applications of Categories, 10(1):1-70, 2002. http://arxiv.org/abs/math/0107188. URL: http://tac.mta.ca/tac/volumes/10/1/10-01abs.html.
http://tac.mta.ca/tac/volumes/10/1/10-01abs.html
Shahn Majid. A Quantum Groups Primer. Cambridge University Press (CUP), 2002. URL: http://dx.doi.org/10.1017/cbo9780511549892.
http://dx.doi.org/10.1017/cbo9780511549892
MathForum. Perko pair knots. URL: http://mathforum.org/mathimages/index.php/Perko_pair_knots.
http://mathforum.org/mathimages/index.php/Perko_pair_knots
Samuel Mimram. Towards 3-dimensional rewriting theory. Logical Methods in Computer Science, 10(2), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(2:1)2014.
http://dx.doi.org/10.2168/LMCS-10(2:1)2014
Bodo Pareigis. In Stefaan Caenepeel and Fred Van Oystaeyen, editors, Hopf Algebras in Noncommutative Geometry and Physics, chapter On Symbolic Computations in Braided Monoidal Categories, pages 269-280. CRC Press, 2004.
Kenneth A. Perko. On the classification of knots. Proceedings of the AMS, 45(2):262-262, 1974. URL: http://dx.doi.org/10.1090/s0002-9939-1974-0353294-x.
http://dx.doi.org/10.1090/s0002-9939-1974-0353294-x
Piotr Pstragowski. On dualizable objects in monoidal bicategories. Master’s thesis, Bonn University, 2014. URL: http://arxiv.org/abs/1411.6691.
http://arxiv.org/abs/1411.6691
Saavedra Rivano. Catégories Tannakiennes, volume 265 of Lecture Notes in Mathematics. Springer Berlin Heidelberg, 1972. URL: http://dx.doi.org/10.1007/bfb0059108.
http://dx.doi.org/10.1007/bfb0059108
Ross Street. Quantum Groups. Cambridge University Press (CUP), 2007. URL: http://dx.doi.org/10.1017/cbo9780511618505.
http://dx.doi.org/10.1017/cbo9780511618505
The Globular Team. Globular documentation. URL: https://ncatlab.org/nlab/show/Globular.
https://ncatlab.org/nlab/show/Globular
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Interaction Automata and the ia2d Interpreter
We introduce interaction automata as a topological model of
computation and present the conceptual plane interpreter ia2d.
Interaction automata form a refinement of both interaction nets and
cellular automata models that combine data deployment, memory
management and structured computation mechanisms. Their local
structure is inspired from pointer machines and allows an asynchronous
spatial distribution of the computation. Our tool can be considered
as a proof-of-concept piece of abstract hardware on which functional
programs can be run in parallel.
Interaction nets
computation models
parallel computation
functional programming
35:1-35:11
Regular Paper
Stéphane
Gimenez
Stéphane Gimenez
David
Obwaller
David Obwaller
10.4230/LIPIcs.FSCD.2016.35
Andrea Asperti, Cecilia Giovannetti, and Andrea Naletto. The bologna optimal higher-order machine. Journal of Functional Programming, 6(6):763-810, 1996. URL: http://dx.doi.org/10.1017/S0956796800001994.
http://dx.doi.org/10.1017/S0956796800001994
Horatiu Cirstea, Germain Faure, Maribel Fernandez, Ian Mackie, and François-Régis Sinot. From functional programs to interaction nets via the rewriting calculus. Electronic Notes in Theoretical Computer Science, 174(10):39-56, 2007.
Maribel Fernández, Ian Mackie, Shinya Sato, and Matthew Walker. Recursive functions with pattern matching in interaction nets. ENTCS, 253(4):55-71, 2009. URL: http://dx.doi.org/10.1016/j.entcs.2009.10.017.
http://dx.doi.org/10.1016/j.entcs.2009.10.017
Stéphane Gimenez. Programmer, calculer et raisonner avec les réseaux de la logique linéaire. PhD thesis, 2009. URL: http://pps.jussieu.fr/~gimenez/these.html.
http://pps.jussieu.fr/~gimenez/these.html
Stéphane Gimenez. Towards generic inductive constructions in systems of nets. In 13th International Workshop on Termination (WST 2013), page 51, 2013.
Stéphane Gimenez and Georg Moser. The complexity of interaction. In POPL, pages 243-255. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837646.
http://dx.doi.org/10.1145/2837614.2837646
Abubakar Hassan, Eugen Jiresch, and Shinya Sato. An implementation of nested pattern matching in interaction nets. arXiv preprint arXiv:1003.4562, 2010.
Abubakar Hassan, Ian Mackie, and Shinya Sato. Interaction nets: programming language design and implementation. Electronic Communications of the EASST, 10, 2008.
Abubakar Hassan and Shinya Sato. Interaction nets with nested pattern matching. Electronic Notes in Theoretical Computer Science, 203(1):79-92, 2008.
Eugen Jiresch. Towards a GPU-based implementation of interaction nets. In DCM, pages 41-53, 2014. URL: http://dx.doi.org/10.4204/EPTCS.143.4.
http://dx.doi.org/10.4204/EPTCS.143.4
Yves Lafont. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 95-108. ACM, 1989.
Yves Lafont. Interaction combinators. Information and Computation, 137(1):69-101, 1997. URL: http://dx.doi.org/10.1006/inco.1997.2643.
http://dx.doi.org/10.1006/inco.1997.2643
Ugo Dal Lago. A short introduction to implicit computational complexity. In Lectures on Logic and Computation - ESSLLI 2010, ESSLLI 2011, pages 89-109, 2011. URL: http://dx.doi.org/10.1007/978-3-642-31485-8_3.
http://dx.doi.org/10.1007/978-3-642-31485-8_3
Sylvain Lippi. Universal hard interaction for clockless computation. Dem Glücklichen schlägt keine Stunde! Fundamenta Informaticae, 91(2):357-394, 2009. URL: http://dx.doi.org/10.3233/FI-2009-0048.
http://dx.doi.org/10.3233/FI-2009-0048
Ian Mackie. Interaction nets for linear logic. Theoretical Computer Science, 247(1-2):83-140, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00198-5.
http://dx.doi.org/10.1016/S0304-3975(00)00198-5
Ian Mackie. Efficient lambda-evaluation with interaction nets. In RTA, volume 3091 of Lecture Notes in Computer Science, pages 155-169, 2004. URL: http://dx.doi.org/10.1007/b98160.
http://dx.doi.org/10.1007/b98160
Ian Mackie and Jorge Sousa Pinto. Encoding linear logic with interaction combinators. Information and Computation, 176(2):153-186, 2002. URL: http://dx.doi.org/10.1006/inco.2002.3163.
http://dx.doi.org/10.1006/inco.2002.3163
Damiano Mazza. Multiport interaction nets and concurrency. In CONCUR, pages 21-35, 2005. URL: http://dx.doi.org/10.1007/11539452_6.
http://dx.doi.org/10.1007/11539452_6
Damiano Mazza. Interaction Nets: Semantics and Concurrent Extensions. PhD thesis, 2006. URL: https://www-lipn.univ-paris13.fr/~mazza/papers/Thesis.pdf.
https://www-lipn.univ-paris13.fr/~mazza/papers/Thesis.pdf
Jorge Sousa Pinto. Sequential and concurrent abstract machines for interaction nets. In FOSSACS, pages 267-282. Springer-Verlag, 2000. URL: http://dx.doi.org/10.1007/3-540-46432-8_18.
http://dx.doi.org/10.1007/3-540-46432-8_18
Jorge Sousa Pinto. Parallel evaluation of interaction nets with MPINE. In RTA, pages 353-356, 2001. URL: http://dx.doi.org/10.1007/3-540-45127-7_26.
http://dx.doi.org/10.1007/3-540-45127-7_26
Jorge Sousa Pinto. Parallel implementation models for the lambda-calculus using the geometry of interaction. In TLCA, pages 385-399, 2001. URL: http://dx.doi.org/0.1007/3-540-45413-6_30.
http://dx.doi.org/0.1007/3-540-45413-6_30
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
The first-order theory of rewriting is decidable for finite left-linear
right-ground rewrite systems. We present a new tool that implements the
decision procedure for this theory. It is based on tree automata
techniques. The tool offers the possibility to synthesize rewrite systems
that satisfy properties that are expressible in the first-order theory of
rewriting.
first-order theory
ground rewrite systems
automation
synthesis
36:1-36:12
Regular Paper
Franziska
Rapp
Franziska Rapp
Aart
Middeldorp
Aart Middeldorp
10.4230/LIPIcs.FSCD.2016.36
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
H. Comon. Sequentiality, monadic second-order logic and tree automata. I&C, 157(1-2):25-51, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2838.
http://dx.doi.org/10.1006/inco.1999.2838
H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications, 2007. URL: http://www.grappa.univ-lille3.fr/tata.
http://www.grappa.univ-lille3.fr/tata
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In Proc. 5th LICS, pages 242-248, 1990. URL: http://dx.doi.org/10.1109/LICS.1990.113750.
http://dx.doi.org/10.1109/LICS.1990.113750
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable (extended version). Technical Report I.T. 197, LIFL, 1990.
E. Jiresch. A term rewriting laboratory with systematic and random generation and heuristic test facilities. Master’s thesis, Vienna University of Technology, 2008. URL: http://www.logic.at/staff/jiresch/thesis/thesis.pdf.
http://www.logic.at/staff/jiresch/thesis/thesis.pdf
J. Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. In Proc. 8th RTA, volume 1232 of LNCS, pages 241-253, 1997. URL: http://dx.doi.org/10.1007/3-540-62950-5_75.
http://dx.doi.org/10.1007/3-540-62950-5_75
A. Stump, H. Zantema, G. Kimmell, and R. El Haj Omar. A rewriting view of simple typing. LMCS, 9(1), 2012. URL: http://dx.doi.org/10.2168/LMCS-9(1:4)2013.
http://dx.doi.org/10.2168/LMCS-9(1:4)2013
R. Treinen. The first-order theory of linear one-step rewriting is undecidable. TCS, 208(1-2):179-190, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(98)00083-8.
http://dx.doi.org/10.1016/S0304-3975(98)00083-8
S. Vorobyov. The undecidability of the first-order theories of one step rewriting in linear canonical systems. I&C, 175(2):182-213, 2002. URL: http://dx.doi.org/10.1006/inco.2002.3151.
http://dx.doi.org/10.1006/inco.2002.3151
H. Zantema. Automatically finding non-confluent examples in term rewriting. In Proc. 2nd IWC, pages 11-15, 2013. URL: http://cl-informatik.uibk.ac.at/iwc/iwc2013.pdf.
http://cl-informatik.uibk.ac.at/iwc/iwc2013.pdf
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode