Abstract
We present a model of recursive and impredicatively quantified types with mutable references. We interpret in this model all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and functional languages. We establish in this purely semantic fashion a soundness proof of the typing systems underlying these TILs and TALs---ensuring that every well-typed program is safe. The technique is generic, and applies to any small-step semantics including λ-calculus, labeled transition systems, and von Neumann machines. It is also simple, and reduces mainly to defining a Kripke semantics of the Gödel-Löb logic of provability. We have mechanically verified in Coq the soundness of our type system as applied to a von Neumann machine.
- Amal Ahmed, Andrew W. Appel, and Roberto Virga. A stratified semantics of general references embeddable in higher-order logic. In 17th Annual IEEE Symp. on Logic in Computer Science, pp. 75--86, June 2002. Google ScholarDigital Library
- Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In POPL '00: 27th acm sigplan-sigact Symp. on Principles of Programming Languages, pp. 243--253, Jan. 2000. Google ScholarDigital Library
- Amal J. Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, Princeton, NJ, Nov. 2004. Tech Report TR-713-04. Google ScholarDigital Library
- Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. on Programming Languages and Systems, 23(5):657--683, Sept. 2001. Google ScholarDigital Library
- Andrew W. Appel. Foundational proof-carrying code. In Symp. on Logic in Computer Science (LICS '01), pp. 247--258. IEEE, 2001. Google ScholarDigital Library
- Bruno Barras et al. The Coq Proof Assistant reference manual. Technical report, INRIA, 1998.Google Scholar
- Michael Barr and Charles Wells. Toposes, Triples and Theories. Grundlehren der math. Wissenschaften. Springer Verlag, 1983. Reprint 12 in Theory and Applications of Category, //www.emis.de/journals/TAC/.Google Scholar
- Karl Crary. Toward a foundational typed assembly language. In POPL '03: 30th ACM Symp. on Principles of Programming Languages, pp. 198--212, 2003. Google ScholarDigital Library
- Juan Chen, Dinghao Wu, Andrew W. Appel, and Hai Fang. A provably sound TAL for back-end optimization. In PLDI '03: Proc. 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 208--219, June 2003. Google ScholarDigital Library
- Saul A. Kripke. Semantical considerations on modal logic. In Proceedings of a Colloquium: Modal and Many Valued Logics, vol. 16, pp. 83--94, 1963.Google Scholar
- John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 1991.Google Scholar
- David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymophic types. Information and Computation, 71(1/2):95--130, 1986. Google ScholarDigital Library
- Paul-André Melliós and Jérôme Vouillon. Recursive polymorphic types and parametricity in an operational framework. In IEEE Symp. on Logic in Computer Science (LICS '05), 2005. Google ScholarDigital Library
- Hiroshi Nakano. A modality for recursion. In LICS '00: 15th Annual Ieee Symp. on Logic in Computer Science, pp. 255--266. Ieee Computer Society Press, 2000. Google ScholarDigital Library
- Hiroshi Nakano. Fixed-point logic with the approximation modality and its Kripke completeness. In Theoretical Aspects of Computer Software, vol. 2215 of LNCS, pp. 165--182. Springer, 2001. Google ScholarDigital Library
- Zhaozhong Ni and Zhong Shao. Certified assembly programming with embedded code pointers. In 33rd ACM Symp. on Principles of Programming Languages, pp. 320--333. ACM Press, Jan. 2006. Google ScholarDigital Library
- Christine Paulin-Mohring. Inductive definitions in the system Coq; rules and properties. In M. Bezem and J. F. Groote, editors,Proc. International Conference on Typed Lambda Calculi and Applications, vol. 664, pp. 328--345. Springer Verlag Lecture Notes in Computer Science, 1993. Google ScholarDigital Library
- Gang Tan and Andrew W. Appel. A compositional logic for control flow. In 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06), pp. 80--94, Jan. 2006. Google ScholarDigital Library
- Gang Tan. A Compositional Logic for Control Flow and its Application to Foundational Proof-Carrying Code. PhD thesis, Princeton University, Princeton, NJ, Aug. 2005. Tech Report CS-TR-731-05. Google ScholarDigital Library
- Dinghao Wu. Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code. PhD thesis, Princeton University, Aug. 2005. Google ScholarDigital Library
- Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. Building certified libraries for PCC: Dynamic storage allocation. In Proc. 2003 European Symp. on Programming (ESOP'03), April 2003. Google ScholarDigital Library
Index Terms
- A very modal model of a modern, major, general type system
Recommendations
A very modal model of a modern, major, general type system
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a model of recursive and impredicatively quantified types with mutable references. We interpret in this model all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and ...
Relational parametricity for references and recursive types
TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementationWe present a possible world semantics for a call-by-value higher-order programming language with impredicative polymorphism, general references, and recursive types. The model is one of the first relationally parametric models of a programming language ...
System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...
Comments