A very modal model of a modern, major, general type system

DOI10.1145/1190216.1190235zbMath1295.68072OpenAlexW4229652664MaRDI QIDQ3189790

Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon, Andrew W. Appel

Publication date: 12 September 2014

Published in: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1190216.1190235

zbMATH Keywords

Kripke modelsrecursive typesmutable referencesimpredicative polymorphism

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items

On the Versatility of Open Logical Relations, Bringing Order to the Separation Logic Jungle, Formally verifying exceptions for low-level code with separation logic, Lewis meets Brouwer: constructive strict implication, Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications, A solution to the PoplMark challenge based on de Bruijn indices, A list-machine benchmark for mechanized metatheory, A relational realizability model for higher-order stateful ADTs, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, A model of PCF in guarded type theory, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, The Essence of Higher-Order Concurrent Separation Logic, Denotational semantics for guarded dependent type theory, Verified Software Toolchain, Temporal refinements for guarded recursive types, Coinduction in Flow: The Later Modality in Fibrations, Multimodal Separation Logic for Reasoning About Operational Semantics, Weak updates and separation logic, A metalanguage for guarded iteration, Unnamed Item, Transfinite Step-Indexing: Decoupling Concrete and Logical Steps, Guarded Dependent Type Theory with Coinductive Types, Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq, Unnamed Item, Unnamed Item, Constructive Modalities with Provability Smack

Uses Software

• Coq