20th International Conference on Types for Proofs and Programs (TYPES 2014), TYPES 2014, May 12-15, 2014, Paris, France
TYPES 2014
May 12-15, 2014
Paris, France
International Conference on Types for Proofs and Programs
TYPES
http://www.types.name/
https://dblp.org/db/conf/types
Leibniz International Proceedings in Informatics
LIPIcs
https://www.dagstuhl.de/dagpub/1868-8969
https://dblp.org/db/series/lipics
1868-8969
Hugo
Herbelin
Hugo Herbelin
Pierre
Letouzey
Pierre Letouzey
Matthieu
Sozeau
Matthieu Sozeau
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
39
2015
978-3-939897-88-0
https://www.dagstuhl.de/dagpub/978-3-939897-88-0
Front Matter, Table of Contents, Preface, Authors Index
Front Matter, Table of Contents, Preface, Authors Index
Front Matter
Table of Contents
Preface
Authors Index
i-x
Front Matter
Hugo
Herbelin
Hugo Herbelin
Pierre
Letouzey
Pierre Letouzey
Matthieu
Sozeau
Matthieu Sozeau
10.4230/LIPIcs.TYPES.2014.i
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory
We study the notions of relative comonad and comodule over a relative comonad. We use these notions to give categorical semantics for the coinductive type families of streams and of infinite triangular matrices and their respective cosubstitution operations in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.
relative comonad
Martin-Löf type theory
coinductive type
computer theorem proving
1-26
Regular Paper
Benedikt
Ahrens
Benedikt Ahrens
Régis
Spadotti
Régis Spadotti
10.4230/LIPIcs.TYPES.2014.1
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, Principles of Programming Languages, pages 27-38. ACM, 2013. URL: http://doi.acm.org/10.1145/2429069.2429075.
http://doi.acm.org/10.1145/2429069.2429075
Peter Aczel. Galois: A Theory Development Project, 1993. Technical Report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks. http://www.cs.man.ac.uk/~petera/papers.html.
http://www.cs.man.ac.uk/~petera/papers.html
Benedikt Ahrens. Modules over relative monads for syntax and semantics. Mathematical Structures in Computer Science, FirstView:1-35, 2014. URL: http://dx.doi.org/10.1017/S0960129514000103.
http://dx.doi.org/10.1017/S0960129514000103
Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17-30, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://hott.github.io/M-types/.
https://hott.github.io/M-types/
Benedikt Ahrens and Régis Spadotti. Terminal semantics for codata types in intensional Martin-Löf type theory: Coq code. URL: http://benediktahrens.github.io/coinductives/.
http://benediktahrens.github.io/coinductives/
Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, volume 6014 of LNCS, pages 297-311. Springer, 2010.
Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed Containers. Unpublished version, URL: http://www.cs.nott.ac.uk/~txa/publ/jcont.pdf.
http://www.cs.nott.ac.uk/~txa/publ/jcont.pdf
Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Proceedings of Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 453-468. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-48168-0_32.
http://dx.doi.org/10.1007/3-540-48168-0_32
Steve Awodey, Nicola Gambino, and Kristina Sojakova. Inductive Types in Homotopy Type Theory. In Proceedings of Symposium on Logic in Computer Science, pages 95-104. IEEE, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.21.
http://dx.doi.org/10.1109/LICS.2012.21
The Coq Development Team. The Coq Proof Assistant. http://coq.inria.fr, 2015.
http://coq.inria.fr
Thierry Coquand. Infinite objects in type theory. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs 1993, volume 806 of Lecture Notes in Computer Science, pages 62-78. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-58085-9_72.
http://dx.doi.org/10.1007/3-540-58085-9_72
Peter Dybjer. Representing Inductively Defined Sets by Wellorderings in Martin-Löf’s Type Theory. Theor. Comput. Sci., 176(1-2):329-335, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00145-4.
http://dx.doi.org/10.1016/S0304-3975(96)00145-4
Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the Symposium on Logic in Computer Science, pages 193-202, Washington, DC, USA, 1999. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.1999.782615.
http://dx.doi.org/10.1109/LICS.1999.782615
André Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Inf. Comput., 208(5):545-564, 2010. URL: http://dx.doi.org/10.1016/j.ic.2009.07.003.
http://dx.doi.org/10.1016/j.ic.2009.07.003
Gérard P. Huet and Amokrane Saïbi. Constructive category theory. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 239-276. The MIT Press, 2000.
Bart Jacobs and Jan Rutten. A tutorial on (co) algebras and (co) induction. Bulletin-European Association for Theoretical Computer Science, 62:222-259, 1997.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
Ralph Matthes and Celia Picard. Verification of redecoration for infinite triangular matrices using coinduction. In Nils Anders Danielsson and Bengt Nordström, editors, Workshop on Types for Proofs and Programs, volume 19 of LIPIcs, pages 55-69. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.5.
http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.5
Ieke Moerdijk and Erik Palmgren. Wellfounded trees in categories. Ann. Pure Appl. Logic, 104(1-3):189-218, 2000. URL: http://dx.doi.org/10.1016/S0168-0072(00)00012-9.
http://dx.doi.org/10.1016/S0168-0072(00)00012-9
John Power. Abstract syntax: Substitution and binders. Electron. Notes Theor. Comput. Sci., 173:3-16, 4 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.024.
http://dx.doi.org/10.1016/j.entcs.2007.02.024
Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in coq. In Gerwin Klein and Ruben Gamboa, editors, Proceedings of Interactive Theorem Proving, volume 8558 of Lecture Notes in Computer Science, pages 499-514. Springer, 2014.
Miki Tanaka and John Power. A unified category-theoretic formulation of typed binding signatures. In Proceedings of the workshop on Mechanized reasoning about languages with variable binding, MERLIN'05, pages 13-24. ACM, 2005. URL: http://doi.acm.org/10.1145/1088454.1088457.
http://doi.acm.org/10.1145/1088454.1088457
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
http://homotopytypetheory.org/book
Tarmo Uustalu and Varmo Vene. The dual of substitution is redecoration. In Kevin Hammond and Sharon Curtis, editors, Scottish Functional Programming Workshop, volume 3 of Trends in Functional Programming, pages 99-110. Intellect, 2001.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A Calculus of Constructions with Explicit Subtyping
The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. We avoid problems related to coercions and dependent types by using the Tarski style of universes and by adding equations to reflect equality.
type theory
calculus of constructions
universes
cumulativity
subtyping
27-46
Regular Paper
Ali
Assaf
Ali Assaf
10.4230/LIPIcs.TYPES.2014.27
Henk Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117-309. Oxford University Press, 1992.
Bruno Barras. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, Université Paris 7, 1999.
Bruno Barras and Benjamin Grégoire. On the role of type decorations in the calculus of inductive constructions. In Luke Ong, editor, Computer Science Logic, number 3634 in Lecture Notes in Computer Science, pages 151-166. Springer Berlin Heidelberg, 2005.
Mathieu Boespflug and Guillaume Burel. CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo. In Proof Exchange for Theorem Proving-Second International Workshop, PxTP, page 44, 2012.
Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, number 4583 in Lecture Notes in Computer Science, pages 102-117. Springer Berlin Heidelberg, 2007.
Herman Geuvers and Freek Wiedijk. A logical framework with explicit conversions. Electronic Notes in Theoretical Computer Science, 199:33-47, February 2008.
Robert Harper and Robert Pollack. Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft. In J. Díaz and F. Orejas, editors, TAPSOFT'89, number 352 in Lecture Notes in Computer Science, pages 241-256. Springer Berlin Heidelberg, 1989.
Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89(1):107-136, October 1991.
Hugo Herbelin and Arnaud Spiwack. The Rooster and the Syntactic Bracket. In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 169-187, Dagstuhl, Germany, 2014. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
Marc Lasson. Réalisabilité et paramétricité dans les systèmes de types purs. PhD thesis, Ecole normale supérieure de Lyon, 2012.
Zhaohui Luo. CC^∞_ ⊂ and its meta theory. Laboratory for Foundations of Computer Science Report ECS-LFCS-88-58, 1988.
Zhaohui Luo. ECC, an extended calculus of constructions. In Fourth Annual Symposium on Logic in Computer Science, 1989. LICS'89, Proceedings, pages 386-395, June 1989.
Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Inc., New York, NY, USA, 1994.
Zhaohui Luo. Notes on universes in type theory. Lecture notes for a talk at Institute for Advanced Study, Princeton (http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf), 2012.
http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984.
Erik Palmgren. On universes in type theory. In Twenty-five years of constructive type theory, pages 191-204. Oxford University Press, October 1998.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
http://homotopytypetheory.org/book
Ronan Saillard. Dedukti: a universal proof checker. In Foundation of Mathematics for Computer-Aided Formalization Workshop, 2013.
Vincent Siles and Hugo Herbelin. Pure type system conversion is always typable. Journal of Functional Programming, 22(02):153-180, 2012.
The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
http://coq.inria.fr/doc
L. S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for pure type systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, number 806 in Lecture Notes in Computer Science, pages 19-61. Springer Berlin Heidelberg, 1994.
Floris van Doorn, Herman Geuvers, and Freek Wiedijk. Explicit convertibility proofs in pure type systems. In Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP'13, pages 25-36, New York, NY, USA, 2013. ACM.
Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Objects and Subtyping in the Lambda-Pi-Calculus Modulo
We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the lambda-Pi-calculus modulo, an extension of the lambda-Pi-calculus with rewriting. This embedding may be used as an example of translation of subtyping. We prove this embedding correct with respect to the operational semantics and the type system of the Object Calculus. We implemented a translation tool from the Object Calculus to Dedukti, a type-checker for the lambda-Pi-calculus modulo.
object
calculus
encoding
dependent type
rewrite system
47-71
Regular Paper
Raphaël
Cauderlier
Raphaël Cauderlier
Catherine
Dubois
Catherine Dubois
10.4230/LIPIcs.TYPES.2014.47
Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. In TACS’94, Theoretical Aspects of Computing Sofware, pages 296-320, 1994.
Martín Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer New York, 1996.
Ali Assaf and Guillaume Burel. Holide. URL: https://www.rocq.inria.fr/deducteam/Holide/index.html.
https://www.rocq.inria.fr/deducteam/Holide/index.html
Mathieu Boespflug and Guillaume Burel. CoqInE : Translating the calculus of inductive constructions into the λΠ-calculus modulo. In International Workshop on Proof Exchange for Theorem Proving, 2012.
Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. The lambda-pi-calculus modulo as a universal proof language. In International Workshop on Proof Exchange for Theorem Proving, 2012.
Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant, and Ronan Saillard. Dedukti: a universal proof checker. URL: http://dedukti.gforge.inria.fr.
http://dedukti.gforge.inria.fr
Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and Computation, 155(1/2):108-133, November 1999.
Guillaume Burel. A shallow embedding of resolution and superposition proofs into the λπ-calculus modulo. In International Workshop on Proof Exchange for Theorem Proving, 2013.
Raphaël Cauderlier. Focalide. URL: https://www.rocq.inria.fr/deducteam/Focalide.
https://www.rocq.inria.fr/deducteam/Focalide
Raphaël Cauderlier. Sigmaid. URL: http://sigmaid.gforge.inria.fr.
http://sigmaid.gforge.inria.fr
Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan. Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts. J. Autom. Reason., 39(1):1-47, July 2007.
Horatiu Cirstea, Claude Kirchner, and Luigi Liquori. Matching Power. In Proceedings of RTA'2001, Lecture Notes in Computer Science. Springer-Verlag, May 2001.
Horatiu Cirstea, Luigi Liquori, and Benjamin Wack. Rewriting calculus with fixpoints: Untyped and first-order systems. In TYPES, volume 3085. Springer, 2003.
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. Maude: Specification and programming in rewriting logic. Manual distributed as documentation of the Maude system, Computer Science Laboratory, SRI International. http://maude.csl.sri.com/manual, January 1999.
http://maude.csl.sri.com/manual
The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
http://coq.inria.fr/doc
Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In Simona Ronchi Della Rocca, editor, TLCA, volume 4583 of LNCS, pages 102-117. Springer, 2007.
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 8312 of LNCS/ARCoSS. Springer, 2013.
Kathleen Fisher, Furio Honsell, and John C. Mitchell. A lambda Calculus of Objects and Method Specialization. Nordic Journal of Computing, 1:3-37, 1994.
J. Nathan Foster and Dimitrios Vytiniotis. A theory of featherweight java in isabelle/hol. Archive of Formal Proofs, March 2006. http://afp.sf.net/entries/FeatherweightJava.shtml, Formal proof development.
http://afp.sf.net/entries/FeatherweightJava.shtml
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, January 1993.
Michael Hedberg. A coherence theorem for martin-löf’s type theory. J. Functional Programming, pages 4-8, 1998.
Ludovic Henrio and Florian Kammüller. A mechanized model of the theory of objects. In MarcelloM. Bonsangue and EinarBroch Johnsen, editors, Formal Methods for Open Object-Based Distributed Systems, volume 4468 of Lecture Notes in Computer Science, pages 190-205. Springer Berlin Heidelberg, 2007.
Ludovic Henrio, Florian Kammüller, Bianca Lutz, and Henry Sudhof. Locally nameless sigma calculus. Archive of Formal Proofs, April 2010. http://afp.sf.net/entries/Locally-Nameless-Sigma.shtml, Formal proof development.
http://afp.sf.net/entries/Locally-Nameless-Sigma.shtml
. Focalize. http://focalize.inria.fr.
Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight java - a minimal core calculus for java and gj. In ACM Transactions on Programming Languages and Systems, pages 132-146, 1999.
Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, and Nicholas Cameron. Encoding featherweight java with assignment and immutability using the coq proof assistant. In Workshop on Formal Techniques for Java-like Programs, FTfJP'12, pages 11-19, New York, NY, USA, 2012. ACM.
Fritz Müller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41(6):293-299, 1992.
R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Selected papers on Automath. Elsevier, Amsterdam, 1994.
Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Programming Language Design and Implementation, 1988.
Frank Pfenning and Carsten Schurmann. System description: Twelf - a meta-logical framework for deductive systems. In International Conference on Automated Deduction (CADE-16), pages 202-206. Springer-Verlag LNAI, 1999.
Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207-247, April 1994.
Jan Zwanenburg. Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow. PhD thesis, Eindhoven University of Technology, 1999.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Typeful Normalization by Evaluation
We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-term with sums and call/cc into a CPS term in normal form, which we express in a typed dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.
Normalization by Evaluation
Generalized Algebraic Data Types
Continuation-Passing Style
partial evaluation
72-88
Regular Paper
Olivier
Danvy
Olivier Danvy
Chantal
Keller
Chantal Keller
Matthias
Puech
Matthias Puech
10.4230/LIPIcs.TYPES.2014.72
Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In Jerzy Marcinkowski, editor, Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), pages 3-12, Wroclaw, Poland, July 2007. IEEE Computer Society Press.
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In Joseph Halpern, editor, Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 203-210, Boston, Massachusetts, June 2001. IEEE Computer Society Press.
Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction-free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter Johnstone, editors, Category Theory and Computer Science, number 953 in Lecture Notes in Computer Science, pages 182-199, Cambridge, UK, August 1995. Springer-Verlag.
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of SAT/SMT solvers to Coq through proof witnesses. In Jouannaud and Shao [45], pages 135-150.
Kenichi Asai. On typing delimited continuations: three new solutions to the printf problem. Higher-Order and Symbolic Computation, 22(3):275-291, 2009.
Kenichi Asai, Luminous Fennell, Peter Thiemann, and Yang Zhang. A type theoretic specification for partial evaluation. In Olaf Chitil, Andy King, and Olivier Danvy, editors, Proceedings of the 16th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'14), pages 57-68, Canterbury, UK, September 2014. ACM Press.
Robert Atkey, Sam Lindley, and Jeremy Yallop. Unembedding domain-specific languages. In Stephanie Weirich, editor, Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009, Edinburgh, Scotland, UK, 3 September 2009, pages 37-48. ACM, 2009.
Vincent Balat. Une étude des sommes fortes: isomorphismes et formes normales. PhD thesis, PPS, Université Denis Diderot (Paris VII), Paris, France, December 2002.
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, SIGPLAN Notices, Vol. 39, No. 1, pages 64-76, Venice, Italy, January 2004. ACM Press.
Vincent Balat and Olivier Danvy. Strong normalization by type-directed partial evaluation and run-time code generation. In Xavier Leroy and Atsushi Ohori, editors, Proceedings of the Second International Workshop on Types in Compilation, number 1473 in Lecture Notes in Computer Science, pages 240-252, Kyoto, Japan, March 1998. Springer-Verlag.
Freiric Barral. Decidability for non standard conversions in typed λ-calculus. PhD thesis, Ludvig-Maximilians-Universität and Université Paul Sabatier, München, Germany and Toulouse, France, June 2008.
Ulrich Berger. Program extraction from normalization proofs. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91-106, Utrecht, The Netherlands, March 1993. Springer-Verlag.
Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg. Program extraction from normalization proofs. Studia Logica, 82(1):25-49, 2006.
Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In Bernhard Möller and John V. Tucker, editors, Prospects for hardware foundations (NADA), number 1546 in Lecture Notes in Computer Science, pages 117-137, Berlin, Germany, 1998. Springer-Verlag.
Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Gilles Kahn, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203-211, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press.
Mathieu Boespflug. Conception d'un noyau de vérification de preuves pour le λΠ-calcul modulo. PhD thesis, École Polytechnique, Palaiseau, France, January 2011.
Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In Jouannaud and Shao [45], pages 362-377.
Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(5):509-543, 2009.
James Cheney and Ralf Hinze. First-class phantom types. Technical Report 1901, Computing and Information Science, Cornell University, Ithaca, New York, 2003.
Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In James Hook and Peter Thiemann, editors, Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP'08), SIGPLAN Notices, Vol. 43, No. 9, pages 143-156, Victoria, British Columbia, September 2008. ACM Press.
Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75-94, 1997.
Djordje Čubrić, Peter Dybjer, and Philip J. Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8:153-192, 1998.
Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183-195, 1994.
Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 242-257, St. Petersburg Beach, Florida, January 1996. ACM Press.
Olivier Danvy. Functional unparsing. Journal of Functional Programming, 8(6):621-625, 1998.
Olivier Danvy. Online type-directed partial evaluation. In Masahiko Sato and Yoshihito Toyama, editors, Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, pages 271-295, Kyoto, Japan, April 1998. World Scientific.
Olivier Danvy and Peter Dybjer, editors. Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE 1998), BRICS Note Series NS-98-8, Gothenburg, Sweden, May 1998. BRICS, Department of Computer Science, Aarhus University. Available online at http://www.brics.dk/~nbe98/programme.html.
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.
Olivier Danvy and Julia L. Lawall. Back to direct style II: First-class continuations. In William Clinger, editor, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 299-310, San Francisco, California, June 1992. ACM Press.
Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. The essence of eta-expansion in partial evaluation. Lisp and Symbolic Computation, 8(3):209-227, 1995.
Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. Eta-expansion does The Trick. ACM Transactions on Programming Languages and Systems, 8(6):730-751, 1996.
Olivier Danvy, Morten Rhiger, and Kristoffer Rose. Normalization by evaluation with typed abstract syntax. Journal of Functional Programming, 11(6):673-680, 2001.
Peter Dybjer and Andrzej Filinski. Normalization and partial evaluation. In Gilles Barthe, Peter Dybjer, Luís Pinto, and João Saraiva, editors, Applied Semantics - Advanced Lectures, number 2395 in Lecture Notes in Computer Science, pages 137-192, Caminha, Portugal, September 2000. Springer-Verlag.
Andrzej Filinski. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151-165, Kraków, Poland, May 2001. Springer.
Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. Journal of Automated Reasoning, 49(2):241-273, 2012.
François Garillot and Benjamin Werner. Simple types in type theory: Deep and shallow encodings. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, number 4732 in Lecture Notes in Computer Science, pages 368-382, Kaiserslautern, Germany, September 2007. Springer.
Jacques Garrigue and Didier Rémy. Ambivalent types for principal type inference with gadts. In Chung-chieh Shan, editor, Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings, volume 8301 of Lecture Notes in Computer Science, pages 257-272. Springer, 2013.
George Gonthier. Formal proof - the four-color theorem. Notices of the AMS, 55(11):1382-1393, December 2008.
Timothy G. Griffin. A formulae-as-types notion of control. In Paul Hudak, editor, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 47-58, San Francisco, California, January 1990. ACM Press.
Peter Hancock. The model of computable terms. In Danvy and Dybjer [27]. Available online at http://www.brics.dk/~nbe98/programme.html.
John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Journal of Functional Programming, 7(3):303-319, 1997.
Noriko Hirota and Kenichi Asai. Formalizing a correctness property of a type-directed partial evaluator. In Nils Anders Danielsson and Bart Jacobs, editors, Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL'14, pages 41-46. ACM, 2014.
Danko Ilik. Constructive Completeness Proofs and Delimited Control. PhD thesis, École Polytechnique, Palaiseau, France, October 2010.
Danko Ilik. A formalized type-directed partial evaluator for shift and reset. In Ugo de'Liguoro and Alexis Saurin, editors, Proceedings of the First Workshop on Control Operators and their Semantics, COS 2013, Eindhoven, The Netherlands, June 24-25, 2013, volume 127 of EPTCS, pages 86-100, 2013.
Jean-Pierre Jouannaud and Zhong Shao, editors. Certified Programs and Proofs - First International Conference, CPP 2011, number 7086 in Lecture Notes in Computer Science, Kenting, Taiwan, December 2011. Springer.
Oleg Kiselyov. Type-safe functional formatted IO, 2008. Web post, available at URL: http://okmij.org/ftp/typed-formatting/.
http://okmij.org/ftp/typed-formatting/
Oleg Kiselyov. Typed tagless final interpreters. In Jeremy Gibbons, editor, Generic and Indexed Programming - International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures, volume 7470 of Lecture Notes in Computer Science, pages 130-174. Springer, 2010.
Per Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. In Proceedings of the Third Scandinavian Logic Symposium (1972), volume 82 of Studies in Logic and the Foundation of Mathematics, pages 81-109. North-Holland, 1975.
Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs - Proceedings, number 193 in Lecture Notes in Computer Science, pages 219-224, Brooklyn, New York, June 1985. Springer.
Chetan R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1990.
Matthias Puech. Parametric HOAS with first-class modules. https://syntaxexclamation.wordpress.com/2014/06/27/parametric-hoas-with-first-class-modules/, 2014.
https://syntaxexclamation.wordpress.com/2014/06/27/parametric-hoas-with-first-class-modules/
John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pages 717-740, Boston, Massachusetts, 1972.
John C. Reynolds. Normalization and functor categories. In Danvy and Dybjer [27]. Available online at http://www.brics.dk/~nbe98/programme.html.
Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Greg Morrisett, editor, Proceedings of the Thirtieth Annual ACM Symposium on Principles of Programming Languages, SIGPLAN Notices, Vol. 38, No. 1, pages 224-235, New Orleans, Louisiana, January 2003. ACM Press.
Jeremy Yallop and Oleg Kiselyov. First-class modules: hidden power and tantalizing promises. Presented at the 2010 Workshop on ML, 2010.
Zhe Yang. Language Support for Program Generation: Reasoning, Implementation, and Applications. PhD thesis, Computer Science Department, New York University, New York, New York, August 2001.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Dialectica Categories and Games with Bidding
This paper presents a construction which transforms categorical models of additive-free propositional linear logic, closely based on de Paiva's dialectica categories and Oliva's functional interpretations of classical linear logic. The construction is defined using dependent type theory, which proves to be a useful tool for reasoning about dialectica categories. Abstractly, we have a closure operator on the class of models: it preserves soundness and completeness and has a monad-like structure. When applied to categories of games we obtain 'games with bidding', which are hybrids of dialectica and game models, and we prove completeness theorems for two specific such models.
Linear logic
Dialectica categories
categorical semantics
model theory
game semantics
dependent types
functional interpretations
89-110
Regular Paper
Jules
Hedges
Jules Hedges
10.4230/LIPIcs.TYPES.2014.89
Jeremy Avigad and Solomon Feferman. Gödel’s functional ("Dialectica") interpretation. In S. Buss, editor, Handbook of proof theory, volume 137 of Studies in logic and the foundations of mathematics, pages 337-405. North Holland, Amsterdam, 1998.
Michael Barr. *-autonomous categories and linear logic. Mathematical structures in computer science, 1(2):159-178, 1991.
Andrej Bauer. The Dialectica interpretation in Coq. Available electronically at http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/, 2011.
P. N. Benton. A mixed linear and non-linear logic: proofs, terms and models (preliminary report). Technical report, University of Cambridge, 1994.
Bodil Biering. Cartesian closed Dialectica categories. Annals of pure and applied logic, 156(2-3):290-307, 2008.
Andreas Blass. A game semantics for linear logic. Annals of pure and applied logic, 1991.
Valeria de Paiva. The dialectica categories. In Proc. of categories in computer science, 1989.
Valeria de Paiva. Categorical multirelations, linear logic and petri nets. Technical report, University of Cambridge, 1991.
Valeria de Paiva. The dialectica categories. Technical report, University of Cambridge, 1991.
Valeria de Paiva. Lineales: algebras and categories in the semantics of linear logic. In D. Barker-Plummer, D. Beaver, Johan van Benthem, and P. Scotto di Luzio, editors, Words, Proofs and Diagrams. CSLI, 2002.
Valeria de Paiva. Dialectica and Chu construtions: Cousins? Theory and applications of categories, 17(7):127-152, 2007.
Pieter Hofstra. The dialectica monad and its cousins. In Models, Logics, and Higher-dimensional Categories: A Tribute to the Work of Mihaly Makkai, volume 53 of CRM Proceedings and Lecture Notes, pages 107-139. American Mathematical Society, 2011.
Martin Hyland. Proof theory in the abstract. Annals of pure and applied logic, 114(1-3):43-78, 2002.
Martin Hyland. Slides of an invited lecture `Fibrations in Logic' at Category Theory 2007, Coimbra, Portrugal. Available electronically at https://www.dpmms.cam.ac.uk/ martin/Research/Slides/ct2007.pdf, 2007.
Martin Hyland and Luke Ong. Fair games and full completeness for multiplicative linear logic without the MIX rule. Unpublished manuscript, 1993.
Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003.
Ulrich Kohlenbach. Applied proof theory: proof interpretations and their use in mathematics. Springer, 2008.
Saunders Mac Lane. Categories for the working mathematician. Springer, 1978.
Maria Emilia Maietti, Paola Maneggia, Valeria de Paiva, and Eike Ritter. Relating categorical semantics for intuitionistic linear logic. Applied categorical structures, 13(1):1-36, 2005.
Paul-André Melliès. Asynchronous games 3: An innocent model of linear logic. Proceedings of the 10th Conference on Category Theory and Computer Science, 2004.
Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional linear logic. Proceedings of the 20th Conference on Logic in Computer Science, 2005.
Paul-André Melliès. Categorical semantics of linear logic. In Interactive models of computation and program behaviour. Société Mathématique de France, 2009.
Alexandre Miquel. A model for impredicative type systems with universes, intersection types and subtyping. In In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00), 2000.
Paulo Oliva. Computational interpretations of classical linear logic. Proceedings of WoLLIC'07, 4576:285-296, 2007.
Paulo Oliva. An analysis of Gödel’s dialectica interpretation via linear logic. Dialectica, 62:269-290, 2008.
Paulo Oliva. Functional interpretations of linear and intuitionistic logic. Information and Computation, 208(5):565-577, 2010.
Philip J. Scott. The "Dialectica" interpretation and categories. Mathematical logic quarterly, 24(31-36):553-575, 1978.
Masaru Shirahata. The dialectica interpretation of first-order classical affine logic. Theory and applications of categories, 2006.
Matthijs Vákár. Syntax and semantics of linear dependent types. Technical report, University of Oxford, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The General Universal Property of the Propositional Truncation
In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega^op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in standard syntactical homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A -> Q and Q -> B.
coherence conditions
propositional truncation
Reedy limits
universal property
well-behaved constancy
111-145
Regular Paper
Nicolai
Kraus
Nicolai Kraus
10.4230/LIPIcs.TYPES.2014.111
Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in homotopy type theory. In Typed Lambda Calculi and Applications (TLCA), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17-30. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015.
Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Infinite structures in type theory: Problems and approaches. Presented at TYPES, Tallinn, Estonia, 20 May 2015. Work in progress, working title.
Steve Awodey. Natural models of homotopy type theory. arXiv preprints, arXiv:1406.3219, Jun 2014.
Steve Awodey and Andrej Bauer. Propositions as [types]. Journal of Logic and Computation, 14(4):447-471, 2004.
Michael Batanin. Monoidal globular categories as a natural environment for the theory of weak n-categories. Advances in Mathematics, 136(1):39-103, 1998.
Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of higher truncations, 2015. In preparation, to appear in Computer Science Logic (CSL).
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, NJ, 1986.
Nicola Gambino and Richard Garner. The identity type weak factorisation system. Theoretical Computer Science, 409:94-109, Dec 2008.
Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, pages 1-16, Mar 2015.
Jason J. Hickey. Formal objects in type theory using very dependent types. In Foundations of Object Oriented Languages 3, 1996.
André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-categories for the homotopy hypothesis in type theory. In Typed Lambda Calculi and Applications (TLCA), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 226-240. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015.
Mark Hovey. Model Categories. Number 63 in Mathematical surveys and monographs. American Mathematical Society, 2007.
Nicolai Kraus. Truncation Levels in Homotopy Type Theory. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2015.
Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Löf type theory, 2014. Submitted to the special issue of TLCA'13.
Tom Leinster. A survey of definitions of n-category. Theory and applications of Categories, 10(1):1-70, 2002.
Peter LeFanu Lumsdaine. Weak omega-categories from intensional type theory. In Typed Lambda Calculi and Applications (TLCA), pages 172-187. Springer-Verlag, 2009.
Peter LeFanu Lumsdaine and Michael A. Warren. The local universes model: an overlooked coherence construction for dependent type theories. Transactions on Computational Logic (TOCL), 16(3), 2015. To appear.
Jacob Lurie. Higher topos theory, volume 170 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2009.
James E. McClure. On semisimplicial sets satisfying the Kan condition. Homology, Homotopy and Applications, 15(1):73-82, 2013.
Matt Oliveri. A formalized interpreter. Blog post, URL: http://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/.
http://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/
Colin Patrick Rourke and Brian Joseph Sanderson. Δ-sets I: Homotopy theory. The Quarterly Journal of Mathematics, 22(3):321-338, 1971.
Graeme Segal. Classifying spaces and spectral sequences. Publications Mathématiques de l'Institut des Hautes Études Scientifiques, 34(1):105-112, 1968.
Michael Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow). Blog post, URL: http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/.
http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/
Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, pages 1-75, Jan 2015.
Ross Street. The algebra of oriented simplexes. Journal of Pure and Applied Algebra, 49(3):283-335, 1987.
The HoTT and UF community. Homotopy type theory mailing list, since 2011. URL: https://groups.google.com/forum/#!aboutgroup/homotopytypetheory.
https://groups.google.com/forum/#!aboutgroup/homotopytypetheory
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study, first edition, 2013.
http://homotopytypetheory.org/book/
Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011.
Vladimir Voevodsky. A simple type system with two identity types, 2013. Unpublished note.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On the Structure of Classical Realizability Models of ZF
The technique of classical realizability is an extension of the method of forcing; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called realizability models. The structure of these models is, in general, much more complicated than that of the particular case of forcing models.
We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical).
By Shoenfield absoluteness theorem, it follows that every true Sigma^1_3 formula is realized by a closed lambda_c-term.
lambda-calculus
Curry-Howard correspondence
set theory
146-161
Regular Paper
Jean-Louis
Krivine
Jean-Louis Krivine
10.4230/LIPIcs.TYPES.2014.146
S. Berardi, M. Bezem, and T. Coquand. On the computational content of the axiom of choice. J. Symb. Logic, 63(2):600-622, 1998.
U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. In Springer, editor, Proc. Logic Colloquium 2001, pages 89-107, 2005.
H.B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958.
T. Griffin. A formulæ-as-type notion of control. In Conf. record 17th A.C.M. Symp. on Principles of Progr. Languages, 1990.
W. Howard. The formulas-as-types notion of construction, pages 479-490. Acad. Press, 1980.
J.-L. Krivine. Realizability algebras : a program to well order ℝ. Logical Methods in Computer Science, 7(3:02):1-47, 2011.
J.-L. Krivine. Realizability algebras II : new models of ZF + DC. Logical Methods in Computer Science, 8(1:10):1-28, 2012.
J.-L. Krivine. Bar recursion in classical realisability : dependent choice and well ordering of ℝ. http://arxiv.org/abs/1502.00112, 2012 (to appear).
J.-L. Krivine. Realizability algebras III : some examples. http://arxiv.org/abs/1210.5065, 2012 (to appear).
http://arxiv.org/abs/1210.5065
T. Streicher. A classical realizability model arising from a stable model of untyped λ-calculus, 2013 (to appear).
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
An Extensional Kleene Realizability Semantics for the Minimalist Foundation
We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semantics we prove that both levels of MF are consistent with the formal Church Thesis CT. Since MF consists of two levels, an intensional one, called mtt, and an extensional one, called emtt, linked by an interpretation, it is enough to build a realizability semantics for the intensional level mtt to get one for the extensional one emtt, too. Moreover, both levels consists of type theories based on versions of Martin-Löf's type theory. Our realizability semantics for mtt is a modification of the realizability semantics by Beeson in 1985 for extensional first order Martin-Löf's type theory with one universe. So it is formalized in Feferman's classical arithmetic theory of inductive definitions, called ID1^. It is called extensional Kleene realizability semantics since it validates extensional equality of type-theoretic functions extFun, as in Beeson's one. The main modification we perform on Beeson's semantics is to interpret propositions, which are defined primitively in MF, in a proof-irrelevant way. As a consequence, we gain the validity of CT. Recalling that extFun+CT+AC are inconsistent over arithmetics with finite types, we conclude that our semantics does not validate the Axiom of Choice AC on generic types. On the contrary, Beeson's semantics does validate AC, being this a theorem of Martin-Löf's theory, but it does not validate CT. The semantics we present here seems to be the best approximation of Kleene realizability for the extensional level emtt. Indeed Beeson's semantics is not an option for emtt since AC on generic sets added to it entails the excluded middle.
Realizability
Type Theory
formal Church Thesis
162-186
Regular Paper
Maria Emilia
Maietti
Maria Emilia Maietti
Samuele
Maschio
Samuele Maschio
10.4230/LIPIcs.TYPES.2014.162
G. Barthes, V. Capretta, and O. Pons. Setoids in type theory. J. Funct. Programming, 13(2):261-293, 2003. Special issue on "Logical frameworks and metalanguages".
M. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, Berlin, 1985.
E. Bishop. Foundations of Constructive Analysis. McGraw-Hill Book Co., 1967.
T. Coquand. Metamathematical investigation of a calculus of constructions. In P. Odifreddi, editor, Logic in Computer Science, pages 91-122. Academic Press, 1990.
S. Feferman. Iterated inductive fixed-point theories: application to Hancock’s conjecture. In Patras Logic Symposion, pages 171-196. North Holland, 1982.
M. Hofmann. Extensional Constructs in Intensional Type Theory. Distinguished Dissertations. Springer, 1997.
J. M. E. Hyland. The effective topos. In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pages 165-216. North-Holland, Amsterdam-New York, 1982.
J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. Bull. Austral. Math. Soc., 88:205-232, 1980.
M. E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009.
M. E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17):445-463, 2013.
M. E. Maietti and G. Rosolini. Quotient completion for the foundation of constructive mathematics. Logica Universalis, 7(3):371-402, 2013.
M. E. Maietti and G. Rosolini. Unifying exact completions. Applied Categorical Structures, DOI 10.1007/s10485-013-9360-5, 2013.
M. E. Maietti and G. Sambin. Toward a minimalist foundation for constructive mathematics. In L. Crosilla and P. Schuster, editor, From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, number 48 in Oxford Logic Guides, pages 91-114. Oxford University Press, 2005.
M. E. Maietti and G. Sambin. Why topology in the Minimalist Foundation must be pointfree. Logic and Logical Philosophy, 22(2):167-199, 2013.
P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1970.
P. Martin-Löf. Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples, 1984.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford, 1990.
P. Odifreddi. Classical recursion theory, volume 125 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., 1989.
E. Palmgren. Bishop’s set theory. Slides for lecture at the TYPES summer school, 2005.
A. S. Troelstra and D. van Dalen. Constructivism in mathematics, an introduction, vol. I. In Studies in logic and the foundations of mathematics. North-Holland, 1988.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Investigating Streamless Sets
In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless.
We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.
Type theory
Constructive Logic
Finite Sets
187-201
Regular Paper
Erik
Parmann
Erik Parmann
10.4230/LIPIcs.TYPES.2014.187
Michael Beeson. Goodman’s theorem and beyond. Pacific Journal of Mathematics, 84(1):1-16, 1979.
M. Bezem, K. Nakata, and T. Uustalu. On streams that are finitely red. Logical Methods in Computer Science, 2011. URL: http://www.cs.ioc.ee/~keiko/papers/finiteness.pdf.
http://www.cs.ioc.ee/~keiko/papers/finiteness.pdf
The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
http://coq.inria.fr/doc
Thierry Coquand and Arnaud Spiwack. Constructively finite? In Contribuciones científicas en honor de Mirian Andrés Gómez, pages 217-230. Universidad de La Rioja, 2010.
Per Martin-Löf. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Proceedings of the Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975.
Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984.
F. P. Ramsey. On a problem of formal logic. Proceedings of the London Mathematical Society, 2(1):264-286, 1930.
F. Richman and G. Stolzenberg. Well quasi-ordered sets. Advances in Mathematics, 97(2):145-153, 1993.
Anne Sjerp Troelstra and Dirk Van Dalen. Constructivism in mathematics, volume 2. Elsevier, 1988.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
http://homotopytypetheory.org/book
Wim Veldman and Marc Bezem. Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, 2(2):193-211, 1993.
Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full. In Interactive Theorem Proving, pages 250-265. Springer, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Nominal Presentation of Cubical Sets Models of Type Theory
The cubical sets model of Homotopy Type Theory introduced by Bezem, Coquand and Huber uses a particular category of presheaves. We show that this presheaf category is equivalent to a category of sets equipped with an action of a monoid of name substitutions for which a finite support property holds. That category is in turn isomorphic to a category of nominal sets equipped with operations for substituting constants 0 and 1 for names. This formulation of cubical sets brings out the potentially useful connection that exists between the homotopical notion of path and the nominal sets notion of name abstraction. The formulation in terms of actions of monoids of name substitutions also encompasses a variant category of cubical sets with diagonals, equivalent to presheaves on Grothendieck's "smallest test category." We show that this category has the pleasant property that path objects given by name abstraction are exponentials with respect to an interval object.
models of dependent type theory
homotopy type theory
cubical sets
nominal sets
monoids
202-220
Regular Paper
Andrew M.
Pitts
Andrew M. Pitts
10.4230/LIPIcs.TYPES.2014.202
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Extensionality of lambda-*
We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that in type theory the notion of extensional equality be identified with the logical equivalence relation defined by induction on type structure.
Extensionality
logical relations
type theory
lambda calculus
reflection
221-250
Regular Paper
Andrew
Polonsky
Andrew Polonsky
10.4230/LIPIcs.TYPES.2014.221
Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS, pages 412-420. IEEE Computer Society, 1999.
Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14, pages 503-515, New York, NY, USA, 2014. ACM.
H. P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 2), pages 117-309. Oxford University Press, Inc., New York, NY, USA, 1992.
Jean-Philippe Bernardy and Marc Lasson. Realizability and parametricity in pure type systems. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, volume 6604 of Lecture Notes in Computer Science, pages 108-122. Springer Berlin Heidelberg, 2011.
Thierry Coquand. Equality and dependent type theory, 2011. URL: http://www.cse.chalmers.se/~coquand/equality.pdf.
http://www.cse.chalmers.se/~coquand/equality.pdf
Peter Dybjer and Anton Setzer. Indexed induction-recursion. In Reinhard Kahle, Peter Schroeder-Heister, and Robert Stärk, editors, Proof Theory in Computer Science, volume 2183 of Lecture Notes in Computer Science, pages 93-113. Springer Berlin Heidelberg, 2001.
Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg, and Anton Setzer. Fibred data types. In LICS, pages 243-252. IEEE Computer Society, 2013.
F. Rabe and K. Sojakova. Logical Relations for a Logical Framework. ACM Transactions on Computational Logic, 2013. to appear.
William W. Tait. Extensional equality in the classical theory of types. In Werner Depauli-Schimanovich, Eckehart Köhler, and Friedrich Stadler, editors, The Foundational Debate, volume 3 of Vienna Circle Institute Yearbook [1995], pages 219-234. Springer Netherlands, 1995.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Restricted Positive Quantification Is Not Elementary
We show that a restricted variant of constructive predicate logic with positive (covariant) quantification is of super-elementary complexity. The restriction is to limit the number of eigenvariables used in quantifier introductions rules to a reasonably usable level. This construction suggests that the known non-elementary decision algorithms for positive logic may actually be best possible.
constructive logic
complexity
automata theory
251-273
Regular Paper
Aleksy
Schubert
Aleksy Schubert
Pawel
Urzyczyn
Pawel Urzyczyn
Daria
Walukiewicz-Chrzaszcz
Daria Walukiewicz-Chrzaszcz
10.4230/LIPIcs.TYPES.2014.251
Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Monika Seisenberger. Minlog: a tool for program extraction supporting algebras and coalgebras. In Proc. of CALCO'11, volume 6859 of LNCS, pages 393-399. Springer, 2011.
Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.
Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pages 73-78. Springer, 2009.
Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.
The Coq Development Team. The Coq Proof Assistant. Reference Manual. INRIA, December 2011.
Gilles Dowek and Ying Jiang. Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theoretical Computer Science, 360(1-3):193-208, 2006.
Gilles Dowek and Ying Jiang. Enumerating proofs of positive formulae. Computer Journal, 52(7):799-807, 2009.
Georges Gonthier. The four colour theorem: Engineering of a formal proof. In D. Kapur, editor, Computer Mathematics, volume 5081 of LNCS. Springer, 2008.
Georges Gonthier. Advances in the formalization of the odd order theorem. In M. van Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk, editors, Interactive Theorem Proving, volume 6898 of LNCS, page 2. Springer, 2011.
Gerwin Klein et al. seL4: Formal verification of an OS kernel. Communications of the ACM, 53(6):107-115, 2010.
Daniel Leivant. Monotonic use of space and computational complexity over abstract structures. Technical Report CMU-CS-89-21, Carnegie Mellon University, 1989.
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009.
Grigori E. Mints. Solvability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers. Steklov Inst., 98:135-145, 1968.
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
Jens Otten. ileanTAP: An intuitionistic theorem prover. In D. Galmiche, editor, Proc. of TABLEAUX'97, volume 1227 of LNCS, pages 307-312. Springer, 1997.
Ivar Rummelhoff. Polymorphic Π 1 Types and a Simple Approach to Propositions, Types and Sets. PhD thesis, University of Oslo, 2007.
Aleksy Schubert, Paweł Urzyczyn, and Daria Walukiewicz-Chrząszcz. Positive logic is not elementary. Presentation at the Highlights conference, 2013.
Aleksy Schubert, Paweł Urzyczyn, and Daria Walukiewicz-Chrząszcz. How hard is positive quantification? In preparation, 2014.
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 LNCS, pages 451-465. Springer, 2015.
Morten H. Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006.
Hao Wang. A variant to Turing’s theory of computing machines. Journal of the ACM, 4(1):63-92, 1957.
Tao Xue and Qichao Xuan. Proof search and counter model of positive minimal predicate logic. ENTCS, 212(0):87-102, 2008.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On Isomorphism of Dependent Products in a Typed Logical Framework
A complete decision procedure for isomorphism of kinds that contain only dependent product, constant Type and variables is obtained. All proofs are done using Z. Luo's logical framework. They can be easily transferred to a large class of type theories with dependent product.
Isomorphism of types
dependent product
logical framework
274-287
Regular Paper
Sergei
Soloviev
Sergei Soloviev
10.4230/LIPIcs.TYPES.2014.274
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
An Intuitionistic Analysis of Size-change Termination
In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change terminating if and only if it has a certain property which can be statically verified from the recursive definition of the program. Their proof of the size-change termination theorem used Ramsey's Theorem for pairs, which is a purely classical result. In 2012 Vytiniotis, Coquand and Wahlsteldt intuitionistically proved a classical variant of the size-change termination theorem by using the Almost-Full Theorem instead of Ramsey's Theorem for pairs. In this paper we provide an intuitionistic proof of another classical variant of the SCT theorem: our goal is to provide a statement and a proof very similar to the original ones. This can be done by using the H-closure Theorem, which differs from Ramsey's Theorem for pairs only by a contrapositive step. As a side result we obtain another proof of the characterization of the functions computed by a tail-recursive SCT program, by relating the SCT Theorem with the Termination Theorem by Podelski and Rybalchenko. Finally, by investigating the relationship between them, we provide a property in the "language" of size-change termination which is equivalent to Podelski and Rybalchenko's termination.
Intuitionism
Ramsey's Theorem
Termination
288-307
Regular Paper
Silvia
Steila
Silvia Steila
10.4230/LIPIcs.TYPES.2014.288
Peter Aczel. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter An introduction to inductive definitions, pages 739-782. Elsevier, 1977.
Thorsten Altenkirch. A formalization of the strong normalization proof for system F in LEGO. In TLCA, pages 13-28, 1993.
Amir M. Ben-Amram. General size-change termination and lexicographic descent. In Torben Mogensen, David Schmidt, and I. Hal Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of LNCS, pages 3-17. Springer-Verlag, 2002.
Stefano Berardi, Paulo Oliva, and Silvia Steila. Proving termination with transition invariants of height omega. CoRR, abs/1407.4692, 2014.
Stefano Berardi and Silvia Steila. Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic. In TYPES, pages 64-83, 2013.
Stefano Berardi and Silvia Steila. Ramsey theorem as an intuitionistic property of well founded relations. In RTA-TLCA, pages 93-107, 2014.
Stefano Berardi, Silvia Steila, and Keita Yokoyama. Notes on H-closure. In preparation.
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In SAS, pages 87-101, 2005.
Thierry Coquand. A direct proof of Ramsey’s Theorem. Author’s website, revised in 2011, 1994.
Paul Erdős and George Szekeres. A combinatorial problem in geometry. Compositio Mathematica, 2:463-470, 1935.
Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In LICS, pages 269-278. IEEE Press, 2011.
Alfons Geser. Relative termination. PhD thesis, Universitat Passau, 1990.
Matthias Heizmann, Neil D. Jones, and Andreas Podelski. Size-change termination and transition invariants. In SAS, pages 22-50, 2010.
Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In POPL, pages 81-92, 2001.
M.H. Löb and S.S. Wainer. Hierarchies of number-theoretic functions. i. Arch. Math. Logic, 13(1-2):39-51, 1970.
David Park. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI-Conference on Theoretical Computer Science, pages 167-183. Springer-Verlag, 1981.
Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. J. of Symb. Comp., 2(4):325-355, 1986.
Andreas Podelski and Andrey Rybalchenko. Transition invariants. In LICS, pages 32-41, 2004.
Frank Plumpton Ramsey. On a problem in formal logic. Proc. London Math. Soc., 30:264-286, 1930.
Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full - adventures in constructive termination. In ITP, pages 250-265, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode