skip to main content
10.1145/2103786.2103797acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Type systems for dummies

Published: 28 January 2012 Publication History

Abstract

We extend Pure Type Systems with a function turning each term M of type A into a dummy |M| of the same type (|.| is not an identity, in that M ≠ |M|). Intuitively, a dummy represents an unknown, canonical object of the given type: dummies are opaque (cannot be internally inspected), and irrelevant in the sense that dummies of a same type are convertible to each other. This latter condition makes convertibility in PTS with dummies (DPTS) stronger than usual, hence raising not trivial consistency issues. DPTS offer an alternative approach to (proof) irrelevance, tagging irrelevant information at the level of terms and not of types, and avoiding the annoying syntactical duplication of products, abstractions and applications into an explicit and an implicit version, typical of systems like ICC*.

References

[1]
A. Abel. Irrelevance in type theory with a heterogeneous equality judgement. In Proceedings of Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Saarbrücken, Germany, volume 6604 of Lecture Notes in Computer Science, pages 57--71. Springer, 2011.
[2]
T. Altenkirch. Constructions, Inductive types and Strong Normalization proof. PhD thesis, University of Edinburgh, UK, 1993.
[3]
T. Altenkirch. Extensional equality in intensional type theory. In LICS, pages 412--420, 1999.
[4]
T. Altenkirch, C. McBride, and J. McKinna. Why dependent types matter. http://sneezy.cs.nott.ac.uk/epigram/, 2005.
[5]
A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. A compact kernel for the Calculus of Inductive Constructions. Sadhana, 34 (1): 71--144, 2009. 10.1007/s12046-009-0003--3.
[6]
A. Asperti, W. Ricciotti, C. S. Coen, and E. Tassi. The matita interactive theorem prover. In Proceedings of the 23rd International Conference on Automated Deduction (CADE-2011), Wroclaw, Poland, volume 6803 of LNCS, 2011.
[7]
H. Barendregt. Lambda Calculi with Types. In Abramsky, Samson and others, editor, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.
[8]
H. Barendregt. The impact of the lambda calculus in logic and computer science. Bulletin of Symbolic Logic, 3 (2): 181--215, 1997.
[9]
B. Barras and B. Bernardo. The implicit calculus of constructions as a programming language with dependent types. In Foundations of Software Science and Computational Structures, 11th International Conference, FoSSaCS 2008, volume 4962 of phLecture Notes in Computer Science, pages 365--379. Springer, 2008.
[10]
G. Barthe. The relevance of proof-irrelevance. In Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, volume 1443 of Lecture Notes in Computer Science, pages 755--768. Springer, 1998.
[11]
S. Berardi. Towards a mathematical analysis of the coquand-huet calculus of constructions and the other systems in barendregt's cube. Technical report, Dept. of Computer Science, Carnegie Mellon Unviersity and Dipartimento di Matemtica, Università di Torino, 1988.
[12]
B. Bernardo. Towards an implicit calculus of inductive constructions. In Emerging Trends section of TPHOLs 2009, To appear, 2009.
[13]
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer Verlag, 2004. ISBN-3--540--20854--2.
[14]
A. Chlipala. An introduction to programming and proving with dependent types in coq. Journal of Formalized Reasoning, 3 (2): 1--93, 2010.
[15]
T. Coquand and J. Gallier. A proof of strong normalization for the theory of constructions using a kripke-like interpretation. In Workshop on Logical Frameworks, Antibes, May 1990, Local Proceedings, 1990.
[16]
G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. J. Autom. Reasoning, 31 (1): 33--72, 2003. 10.1007/3-540-46508-1_1.
[17]
J. Gallier. On girard's "candidates de reductibilité". In P. Odifreddi, editor, Logic and Computer Science, pages 123--203. Academic Press, 1990.
[18]
H. Geuvers. phLogics and Type Systems. Ph.D. dissertation, Catholic University Nijmegen, 1993.
[19]
H. Geuvers. A short and flexible proof of strong normalization for the calculus of constructions. In P. Dybjer, B. Nordström, and J. M. Smith, editors, Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6--10, 1994, Selected Papers, volume 996 of phLecture Notes in Computer Science, pages 14--38, Berlin, Germany, 1995. Springer.
[20]
H. Geuvers and M.-J. Nederhof. Modular proof of strong normalization for the calculus of constructions. J. Funct. Program., 1 (2): 155--189, 1991.
[21]
J.-Y. Girard. Une extension de l'interprétation de gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the 2nd Scandinavian Logic Symposium, University of Oslo, 1970, volume 63 of phStudies in logic and the foundations of mathematics, pages 63--92, Amsterdam, The Netherlands, 1971. North-Holland.
[22]
G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. sel4: formal verification of an operating-system kernel. phCommun. ACM, 53 (6): 107--115, 2010.
[23]
X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52 (7): 107--115, 2009.
[24]
P. Letouzey. A New Extraction for Coq. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24--28, 2002, volume 2646 of Lecture Notes in Computer Science. Springer-Verlag, 2003.
[25]
W. Lovas and F. Pfenning. Refinement types for logical frameworks and their interpretation as proof irrelevance. Logical Methods in Computer Science, May 2010. To appear.
[26]
Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.
[27]
C. McBride. Elimination with a motive. In Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8--12, 2000, Selected Papers, volume 2277 of Lecture Notes in Computer Science, pages 197--216. Springer, 2000.
[28]
P.-A. Melliès and B. Werner. A generic normalisation proof for pure type systems. In E. Giménez and C. Paulin-Mohring, editors, pTypes for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15--19, 1996, Selected Papers, volume 1512 of Lecture Notes in Computer Science, pages 254--276, Berlin, Germany, 1998. Springer.
[29]
A. Miquel and B. Werner. The not so simple proof-irrelevant model of CC. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs: International Workshop, TYPES 2002, volume 2646 of phLecture Notes in Computer Science, pages 240--258. Springer-Verlag, 2003.
[30]
N. Mishra-Linger and T. Sheard. Erasure and polymorphism in pure type systems. In Proceedings od Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Budapest, Hungary, volume 4962 of phLecture Notes in Computer Science, pages 350--364. Springer, 2008.
[31]
G. C. Necula. Proof-Carrying Code. In P. Lee, F. Henglein, and N. Jones, editors, POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 106--119, New York, NY, USA, 1997. ACM.
[32]
C.-H. L. Ong and E. Ritter. A generic strong normalization argument: Application to the calculus of constructions. In E. Börger, Y. Gurevich, and K. Meinke, editors, phComputer Science Logic, 7th Workshop, CSL'93, Swansea, United Kingdom, September 13--17, 1993, Selected Papers, volume 832 of phLecture Notes in Computer Science, pages 261--279, Berlin, Germany, 1994. Springer.
[33]
S. Owre and N. Shankar. The formal semantics of pvs. Technical Report CSL-97--2R, SRI Technical Report, Revised March 1999.
[34]
F. Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In J. Halpern, editor, Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 221--230, Boston, Ma, USA, June 2001. IEEE Computer Society Press.
[35]
J. Reed. Proof irrelevance and strict definitions in a logical framework. Technical Report Senior Thesis, Carnegie Mellon University-CS-02--153, Carnegie Mellon Unviersity Technical Report, 2002.
[36]
M. H. Sorensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149. Elsevier, 2006.
[37]
J. Souyris, V. Wiels, D. Delmas, and H. Delseny. Formal verification of avionics software products. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, volume 5850 of phLecture Notes in Computer Science, pages 532--546. Springer, 2009.
[38]
W. W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, Symposium on Logic Held at Boston, 1972--73, volume 453 of phLecture Notes in Mathematics, pages 240--251, Berlin, Germany, 1975. Springer.
[39]
M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118 (1): 120--127, 1995.
[40]
J. Terlouw. Strong normalization in type systems: A model theoretical approach. Annals of Pure and Applied Logic, 73 (1): 53--78, 1995. A Tribute to Dirk van Dalen.
[41]
Development Team(2010)}CoqManualThe Coq Development Team. The Coq proof assistant reference manual. \\http://coq.inria.fr/refman/, 2010.
[42]
J. Torlouw. Een nadere bewijstheoretische analyse van GSTT's. Technical report, Dept.of Computer Science, University of Nijmegen, 1989.
[43]
B. Werner. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, 4 (3), 2008.
[44]
J. Yang and C. Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In phProceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, pages 99--110. ACM, 2010.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
TLDI '12: Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation
January 2012
110 pages
ISBN:9781450311205
DOI:10.1145/2103786
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]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 January 2012

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. canonical element
  2. proof irrelevance
  3. pure type system

Qualifiers

  • Research-article

Conference

POPL '12
Sponsor:

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 165
    Total Downloads
  • Downloads (Last 12 months)5
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

View Options

Login options

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