POPLMark reloaded: Mechanizing proofs by logical relations
From MaRDI portal
Publication:5110924
DOI10.1017/S0956796819000170zbMath1442.68257OpenAlexW2995917016WikidataQ113857457 ScholiaQ113857457MaRDI QIDQ5110924
Brigitte Pientka, Kathrin Stark, Andreas Abel, Guillaume Allais, Alberto Momigliano, Aliya Hameer, Steven Schäfer
Publication date: 26 May 2020
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796819000170
Theory of programming languages (68N15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (7)
Rensets and renaming-based recursion for syntax with bindings extended version ⋮ A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda ⋮ Harpoon: mechanizing metatheory interactively ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Linear logical relations and observational equivalences for session-based concurrency
- Data structures and program transformation
- Kripke-style models for typed lambda calculus
- Program extraction from normalization proofs
- Verifying termination and reduction properties about higher-order logic programs
- Inductive families
- A linear logical framework
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- A formal equational theory for call-by-push-value
- The locally nameless representation
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Strongly typed term representations in Coq
- A Formalized Proof of Strong Normalization for Guarded Recursive Types
- Type Theory Should Eat Itself
- Type theory in type theory using quotient inductive types
- Normalization for the Simply-Typed Lambda-Calculus in Twelf
- On Irrelevance and Algorithmic Equality in Predicative Type Theory
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations
- Copatterns
- The power of parameterization in coinductive proof
- A universe of binding and computation
- Programming with binders and indexed data-types
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Proof search specifications of bisimulation and modal logics for the π-calculus
- Mechanizing the metatheory of LF
- Friends with Benefits
- Towards a mechanized metatheory of standard ML
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- Dependently Typed Programming in Agda
- A framework for defining logics
- αCheck: A mechanized metatheory model checker
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Mechanizing proofs with logical relations – Kripke-style
- Explicit substitutions
- F-ing modules
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Categorical reconstruction of a reduction free normalization proof
- Strong normalization of substitutions
- The gentle art of levitation
- A fresh look at programming with names and binders
- Binders unbound
- Monads need not be endofunctors
- Parametric higher-order abstract syntax for mechanized semantics
- Relative Monads Formalised
- A case study in programming coinductive proofs: Howe’s method
- On equivalence and canonical forms in the LF type theory
- Contextual modal type theory
- CakeML
- Theorem Proving in Higher Order Logics
- Intensional interpretations of functionals of finite type I
- Foundations of Software Science and Computational Structures
- Types for Proofs and Programs
- Types for Proofs and Programs
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Psi-calculi in Isabelle
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Types for Proofs and Programs
- Types for Proofs and Programs
This page was built for publication: POPLMark reloaded: Mechanizing proofs by logical relations
