Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma
Pages 2 - 15
Abstract
Intrinsically typed syntax is an important and popular method for mechanized reasoning about programming languages. We explore the limits of this method in the setting of finitely-stratified System F using the Agda proof assistant. This system supports elegant definitions of denotational semantics as well as big-step operational semantics based on intrinsically typed syntax. While its syntactic metatheory (i.e., type soundness) works well, we demonstrate that its semantic metatheory poses technical challenges, by defining a logical relation and proving its fundamental lemma. Our logical relation connects a denotational semantics with an operational one, which exposes issues with transfer lemmas as well as minor issues with universe polymorphism.
References
[1]
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. 2019. POPLMark reloaded: Mechanizing Proofs by Logical Relations. J. Funct. Program., 29 (2019), e19. https://doi.org/10.1017/S0956796819000170
[2]
Andreas Abel, Joakim Öhman, and Andrea Vezzosi. 2018. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2, POPL (2018), 23:1–23:29. https://doi.org/10.1145/3158111
[3]
Amal Ahmed. 2023. OPLSS 2023: Logical Relations. June, Lecture Notes
[4]
Guillaume Allais, James Chapman, Conor McBride, and James McKinna. 2017. Type-and-scope safe programs and their proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, Paris, France. 195–207. https://doi.org/10.1145/3018610.3018613
[5]
Thorsten Altenkirch and Ambrus Kaposi. 2016. 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, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 18–29. https://doi.org/10.1145/2837614.2837638
[6]
Thorsten Altenkirch and Bernhard Reus. 1999. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Computer Science Logic, CSL ’99, 8th Annual Conference of the EACSL, Jörg Flum and Mario Rodríguez-Artalejo (Eds.) (Lecture Notes in Computer Science, Vol. 1683). Springer, Madrid, Spain. 453–468. https://doi.org/10.1007/3-540-48168-0_32
[7]
Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. May, https://www.researchgate.net/publication/2610129 unpublished manuscript
[8]
Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride. 2012. Strongly Typed Term Representations in Coq. J. Autom. Reason., 49, 2 (2012), 141–159. https://doi.org/10.1007/s10817-011-9219-0
[9]
Richard S. Bird and Lambert G. L. T. Meertens. 1998. Nested Datatypes. In Mathematics of Program Construction, MPC’98, Johan Jeuring (Ed.) (Lecture Notes in Computer Science, Vol. 1422). Springer, Marstrand, Sweden. 52–67. https://doi.org/10.1007/BFb0054285
[10]
Richard S. Bird and Ross Paterson. 1999. De Bruijn Notation as a Nested Datatype. J. Funct. Program., 9, 1 (1999), 77–91. https://doi.org/10.1017/s0956796899003366
[11]
James Chapman. 2008. Type Theory Should Eat Itself. In Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008, Andreas Abel and Christian Urban (Eds.) (Electronic Notes in Theoretical Computer Science, Vol. 228). Elsevier, 21–36. https://doi.org/10.1016/J.ENTCS.2008.12.114
[12]
James Chapman, Roman Kireev, Chad Nester, and Philip Wadler. 2019. System F in Agda, for Fun and Profit. In Mathematics of Program Construction - 13th International Conference, MPC 2019, Graham Hutton (Ed.) (Lecture Notes in Computer Science, Vol. 11825). Springer, Porto, Portugal. 255–297. https://doi.org/10.1007/978-3-030-33636-3_10
[13]
James Cheney and Ralf Hinze. 2003. First-Class Phantom Types. Cornell University. https://ecommons.cornell.edu/handle/1813/5614
[14]
Nils Anders Danielsson. 2006. A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. In Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, Thorsten Altenkirch and Conor McBride (Eds.) (Lecture Notes in Computer Science, Vol. 4502). Springer, 93–109. https://doi.org/10.1007/978-3-540-74464-1_7
[15]
Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. Log. Methods Comput. Sci., 7, 2 (2011), https://doi.org/10.2168/LMCS-7(2:16)2011
[16]
Jean-Yves Girard. 1972. Interpreétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Ph. D. Dissertation. Paris.
[17]
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 (2018), e20. https://doi.org/10.1017/S0956796818000151
[18]
Wen Kokke, Jeremy G. Siek, and Philip Wadler. 2020. Programming language foundations in Agda. Sci. Comput. Program., 194 (2020), 102440. https://doi.org/10.1016/j.scico.2020.102440
[19]
Daniel Leivant. 1991. Finitely Stratified Polymorphism. Inf. Comput., 93, 1 (1991), 93–113. https://doi.org/10.1016/0890-5401(91)90053-5
[20]
Conor McBride. 2000. Elimination with a Motive. In Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.) (Lecture Notes in Computer Science, Vol. 2277). Springer, 197–216. https://doi.org/10.1007/3-540-45842-5_13
[21]
Ulf Norell. 2007. Towards a Practical Programming Language based on Dependent Type Theory. Ph. D. Dissertation. Chalmers University of Technology.
[22]
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2018. Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang., 2, POPL (2018), 16:1–16:34. https://doi.org/10.1145/3158104
[23]
John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, Bernard J. Robinet (Ed.) (Lecture Notes in Computer Science, Vol. 19). Springer, 408–423. https://doi.org/10.1007/3-540-06859-7_148
[24]
John C. Reynolds. 1975. User-defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction. In New Directions in Algorithmic Languages, Stephen A. Schumann (Ed.). INRIA, St. Pierre-de-Chartreuse. 309–317. Reprinted in Reynolds1994
[25]
Arjen Rouvoet. 2021. Correct by Construction Language Implementations. Ph. D. Dissertation. Delft University of Technology, Netherlands. https://doi.org/10.4233/uuid:f0312839-3444-41ee-9313-b07b21b59c11
[26]
Arjen Rouvoet, Robbert Krebbers, and Eelco Visser. 2021. Intrinsically typed compilation with nameless labels. Proc. ACM Program. Lang., 5, POPL (2021), 1–28. https://doi.org/10.1145/3434303
[27]
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 2020. Intrinsically-typed definitional interpreters for linear, session-typed languages. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, New Orleans, LA, USA. 284–298. https://doi.org/10.1145/3372885.3373818
[28]
David A. Schmidt. 1986. Denotational Semantics, A Methodology for Software Development. Allyn and Bacon, Inc, Massachusetts. https://people.cs.ksu.edu/~schmidt/text/ds0122.pdf
[29]
Lau Skorstengaard. 2019. An Introduction to Logical Relations. CoRR, abs/1907.11133 (2019), arXiv:1907.11133. arxiv:1907.11133
[30]
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2024. A Logical Approach to Type Soundness. Jan., Manuscript available on iris-project.org
[31]
Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter D. Mosses. 2022. Intrinsically-typed definitional interpreters à la carte. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), 1903–1932. https://doi.org/10.1145/3563355
Index Terms
- Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma
Recommendations
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and ProofsCall-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...
Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer ScienceWe propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types. Our framework subsumes step indexed realizability semantics by untyped ...
A Typed C11 Semantics for Interactive Theorem Proving
CPP '15: Proceedings of the 2015 Conference on Certified Programs and ProofsWe present a semantics of a significant fragment of the C programming language as described by the C11 standard. It consists of a small step semantics of a core language, which uses a structured memory model to capture subtleties of C11, such as strict-...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.
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 the author(s) 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
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 28 August 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
TyDe '24
Sponsor:
TyDe '24: 9th ACM SIGPLAN International Workshop on Type-Driven Development
September 6, 2024
Milan, Italy
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 116Total Downloads
- Downloads (Last 12 months)116
- Downloads (Last 6 weeks)19
Reflects downloads up to 27 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in