skip to main content
research-article

The formal system λδ

Published: 06 November 2009 Publication History

Abstract

The formal system λδ is a typed λ-calculus that pursues the unification of terms, types, environments, and contexts as the main goal. λδ takes some features from the Automath-related λ-calculi and some from the pure type systems, but differs from both in that it does not include the Π construction while it provides for an abbreviation mechanism at the level of terms. λδ enjoys some important desirable properties such as the confluence of reduction, the correctness of types, the uniqueness of types up to conversion, the subject reduction of the type assignment, the strong normalization of the typed terms, and, as a corollary, the decidability of type inference problem.

Supplementary Material

Guidi Appendix (a5-guidi-apndx.pdf)
Online appendix to the formal system λΔ. The appendix supports the information on article 5.

References

[1]
Asperti, A. and Guerrini, S. 1999. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol. 45. Cambridge University Press, Cambridge.
[2]
Asperti, A., Padovani, L., Sacerdoti Coen, C., Guidi, F., and Schena, I. 2003. Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38, 1, 27--46.
[3]
Asperti, A., Sacerdoti Coen, C., Tassi, E., and Zacchiroli, S. 2006. User interaction with the Matita proof assistant. J. Autom. Reason. (Special Issue on User Interfaces for Theorem Proving). To appear.
[4]
Barendregt, H. 1993. Lambda calculi with types. Osborne Handbooks Logic Comput. Sci. 2, 117--309.
[5]
Barras, B. 1996. Coq en Coq. Rapport de Recherche 3026, INRIA.
[6]
Cescutti, D. 2001. Normalizzazione forte attraverso un'interpretazione negli insiemi saturi. M.S. thesis, University of Padova.
[7]
Church, A. 1941. The Calculi of Lambda-Conversion. Annals of Mathematics Studies, Vol. 6. Princeton University Press, Princeton, NJ.
[8]
Coq development team. 2007. The Coq Proof Assistant Reference Manual Version 8.1pl3. INRIA, Orsay.
[9]
Coquand, T. 1985. Une théorie des constructions. Ph.D. thesis, Universite Paris 7.
[10]
Coquand, T. and Huet, G. 1988. The calculus of constructions. Inform. Comput. 76, 2-3, 95--120.
[11]
Coquand, T. and Paulin-Mohring, C. 1990. Inductively defined types. In Proceedings of the International Conference on Computer Logic (Colog'88). P. Martin-Löf and G. Mints, Eds. Lecture Notes in Computer Science, vol. 417. Springer, Berlin.
[12]
Curien, P. and Herbelin, H. 2000. The duality of computation. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), revised ed. ACM SIGPLAN Not. 35, 9. ACM Press, New York, 233--243.
[13]
de Bruijn, N. 1991. A plea for weaker frameworks. In Logical Frameworks. Cambridge University Press, Cambridge, MA, 40--67.
[14]
de Bruijn, N. 1993. Algorithmic definition of lambda-typed lambda calculus. In Logical Environments. Cambridge University Press, Cambridge, MA, 131--145.
[15]
de Bruijn, N. 1994a. Example of a text written in Automath. In Selected Papers on Automath. North-Holland, Amsterdam, 687--700.
[16]
de Bruijn, N. 1994b. Lambda calculus notation with nameless dummies, A tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Selected Papers on Automath. North-Holland, Amsterdam, 375--388.
[17]
de Bruijn, N. 1994c. The mathematical language Automath, its usage, and some of its extensions. In Selected Papers on Automath. North-Holland, Amsterdam, 73--100.
[18]
de Groote, P. 1993. Defining λ-typed λ-calculi by axiomatising the typing relation. In Proceedings of the 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS'93). Lecture Notes in Computer Scince, vol. 665. Springer, Berlin, 712--723.
[19]
de Vrijer, R. 1994. Big trees in a λ-calculus with λ-expressions as types. In Selected Papers on Automath. North-Holland, Amsterdam, 469--492.
[20]
Girard, J.-Y., Taylor, P., and Lafont, Y. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge, MA.
[21]
Guidi, F. 2006. Lambda-Types on the lambda-calculus with abbreviations: A certified specification. Tech. rep. UBLCS 2006-01, University of Bologna. http://www.cs.unibo.it/pub/TR/UBLCS/2006/2006-01.pdf.
[22]
Guidi, F. 2007a. lambda-delta. Formal specification with the proof assistant coq. http://helm.cs.unibo.it/lambda-delta/.
[23]
Guidi, F. 2007b. Procedural representation of CIC proof terms. In Local Proceedings of Programming Languages for Mechanized Mathematics Workshop (PLMMS'07). RISC-LINZ Report Series 07-10 (3120), J. Carette and F. Wiediejk, Eds. 36--52. http://www.risc.uni-linz.ac.at/publications/download/risc_3120/PLMMS_proc.pdf.
[24]
Hendriks, D. and van Oostrom, V. 2003. Adbmal. In Proceedings of the 19th Conference on Automated Deduction (CADE 19). Lecture Notes in Artificial Intelligence, vol. 2741. Springer, Heidelberg, 136--150.
[25]
Jacobs, B. 1999. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier, Amsterdam.
[26]
Jensen, K. and Wirth, N. 1981. PASCAL—User Manual and Report. ISO Pascal Standard. Italian Ed. Gruppo Editoriale Jackson, Milano.
[27]
Kamareddine, F. 2005. Typed λ-calculi with one binder. J. Funct. Program. 15, 5, 771--796.
[28]
Kamareddine, F. and Bloo, R. 2005a. De Bruijn's syntax and reductional behaviour of lambda terms: The typed case. J. Logic Algebraic Program. 62, 2, 159--189.
[29]
Kamareddine, F. and Bloo, R. 2005b. De Bruijn's syntax and reductional behaviour of lambda terms: The untyped case. J. Logic Algebraic Program. 62, 1, 109--131.
[30]
Kamareddine, F., Bloo, R., and Nederpelt, R. 1999. On π-conversion in the λ-cube and the combination with abbreviations. Ann. Pure. Appi. Logic, 97, 1-3, 27--45.
[31]
Kamareddine, F., Laan, T., and Nederpelt, R. 2004. A Modern Perspective on Type Theory From its Origins Until Today. Applied Logic Series, vol. 29. Kluwer Academic Publishers, Norwell, MA.
[32]
Kamareddine, F. and Nederpelt, R. 1996a. Canonical typing and π-conversion in the Barendregt cube. J. Funct. Program. 6, 2, 245--267.
[33]
Kamareddine, F. and Nederpelt, R. 1996b. A useful λ-notation. Theoretical Comput. Sci. 155, 1, 85--109.
[34]
Kleene, S. 1945. On the interpretation of intuitionistic number theory. J. Symbol. Logic 10, 109--124.
[35]
Letouzey, P. and Schwichtenberg, H. 2004. A normalization proof a la Tait for simply-typed lambda-calculus. Formal specification with the proof assistant coq. http://coq.inria.fr/contribs/tait.html.
[36]
Loader, R. 1998. Notes on simply typed lambda calculus. Course Notes Version 1.8.
[37]
Luo, Z. 2003. Pal+: A lambda-free logical framework. J. Funct. Program. 13, 2, 317--338.
[38]
Maietti, M. and Sambin, G. 2005. Towards a minimalist foundation for constructive mathematics. In From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, L. Crosilla and P. Schuster, Eds. Oxford Logic Guides, vol. 48. Oxford University Press, Oxford, UK, 91--114.
[39]
Martin-Löf, P. 1984. Intuitionistic Type Theory (notes by G. Sambin). Studies in Proof Theory, vol. 1. Bibliopolis, Napoli.
[40]
Nederpelt, R. 1994. Strong normalization in a typed lambda calculus with lambda structured types. In Selected Papers on Automath. North-Holland, Amsterdam, 389--468.
[41]
Nederpelt, R., Geuvers, J., and de Vrijer, R., Eds. 1994. Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol. 133. North-Holland, Amsterdam.
[42]
Network Working Group. 1998. Uniform resource identifiers (URI): Generic syntax. RCF 2396. http://www.ietf.org/rfc/rfc2396.txt.
[43]
Nordström, B., Petersson, K., and Smit, J. 1990. Programming in Martin-Löf's Type Theory—An Introduction. Clarendon Press, Oxford, UK.
[44]
Raffalli, C. 2007a. PML: A new proof assistant. In Proceedings of the Types Conference.
[45]
Raffalli, C. 2007b. PML: A new proof assistant and deduction system. In Proceedings of the Workshop on Programming Languages for Mechanized Mathematics (PLMMS'07).
[46]
Raffalli, C. 2008. PML and strong normalisation. In Proceedings of the Types Conference.
[47]
Sørensen, M. and Urzyczyn, P. 2006. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 149. Elsevier, Amsterdam.
[48]
Solmi, R. 2005. Whole platform. Ph.D. thesis UBLCS 2005-07, University of Bologna. http://whole.sourceforge.net/.
[49]
van Benthem Jutting, L. 1994a. Checking Landau's Grundlagen in the Automath system. In Selected Papers on Automath. North-Holland, Amsterdam, 299--301,701--720,721--732,763--799, 805--808.
[50]
van Benthem Jutting, L. 1994b. Description of AUT-68. In Selected Papers on Automath. North-Holland, Amsterdam, 251--273.
[51]
van Benthem Jutting, L. 1994c. The language theory of λ, a typed λ-calculus where terms are types. In Selected Papers on Automath. North-Holland, Amsterdam, 655--683.
[52]
van Daalen, D. 1980. The language theory of Automath. Ph.D. thesis, Eindhoven University of Technology.
[53]
van Oostrom, V. 2002. Simply typed lambda calculus is strongly normalising. Typescript note. http://www.phil.uu.nl/~oostrom/.
[54]
Wiedijk, F. 1999. A lambda-typed typed lambda calculus with infinitely many lambdas. Typescript note. http://www.cs.ru.nl/~freek/.

Cited By

View all
  • (2015)ELPIProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_32(460-468)Online publication date: 24-Nov-2015

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic
ACM Transactions on Computational Logic  Volume 11, Issue 1
October 2009
270 pages
ISSN:1529-3785
EISSN:1557-945X
DOI:10.1145/1614431
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 November 2009
Accepted: 01 July 2008
Revised: 01 May 2008
Received: 01 November 2006
Published in TOCL Volume 11, Issue 1

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Abbreviations
  2. environments as terms
  3. terms as types

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2015)ELPIProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_32(460-468)Online publication date: 24-Nov-2015

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media