Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMath1152.68516OpenAlexW2484880499MaRDI QIDQ5477646

Geoffrey Washburn, Peter Sewell, Matthew W. Fairbairn, Aaron Bohannon, Benjamin C. Pierce, Stephanie Weirich, Dimitrios Vytiniotis, J. Nathan Foster, Brian E. Aydemir, Steve Zdancewic

Publication date: 6 July 2006

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Related Items

Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ Modular verification of chemical reaction network encodings via serializability analysis ⋮ Coq formalization of the higher-order recursive path ordering ⋮ Directly reflective meta-programming ⋮ A Rewriting Logic Approach to Type Inference ⋮ A two-level logic approach to reasoning about computations ⋮ Formalizing semantic bidirectionalization and extensions with dependent types ⋮ Mechanized Verification of CPS Transformations ⋮ αCheck: A mechanized metatheory model checker ⋮ Mechanizing type environments in weak HOAS ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Variable binding and substitution for (nameless) dummies ⋮ The locally nameless representation ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ A solution to the PoplMark challenge based on de Bruijn indices ⋮ Nested abstract syntax in Coq ⋮ Formal metatheory of programming languages in the Matita interactive theorem prover ⋮ A list-machine benchmark for mechanized metatheory ⋮ ASP\(_{\text{fun}}\) : a typed functional active object calculus ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Romeo: A system for more flexible binding-safe programming ⋮ Unnamed Item ⋮ Psi-calculi in Isabelle ⋮ Nominal techniques in Isabelle/HOL ⋮ The Abella Interactive Theorem Prover (System Description) ⋮ Nominal Inversion Principles ⋮ Nominal Lawvere theories: a category theoretic account of equational theories with names ⋮ Derivation and inference of higher-order strictness types ⋮ Multimodal Separation Logic for Reasoning About Operational Semantics ⋮ Modules over monads and initial semantics ⋮ A verified framework for higher-order uncurrying optimizations ⋮ Structural Abstract Interpretation: A Formal Study Using Coq ⋮ A computer-verified monadic functional implementation of the integral ⋮ Programming Inductive Proofs ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ The Matita Interactive Theorem Prover ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Explicit Contexts in LF (Extended Abstract) ⋮ Unnamed Item ⋮ A formalization of multi-tape Turing machines ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ PoplMark ⋮ Formalizing Operational Semantic Specifications in Logic ⋮ Mechanizing the Metatheory of mini-XQuery ⋮ Mechanized metatheory revisited ⋮ Proof assistants: history, ideas and future ⋮ Term-generic logic ⋮ Free Theorems and Runtime Type Representations ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi ⋮ Mechanizing metatheory without typing contexts

Uses Software