Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477646
DOI10.1007/11541868zbMATH Open1152.68516OpenAlexW2484880499MaRDI QIDQ5477646FDOQ5477646
Geoffrey Washburn, Peter Sewell, M. Fairbairn, Aaron Bohannon, Benjamin C. Pierce, Stephanie Weirich, Dimitrios Vytiniotis, J. Nathan Foster, Brian 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
Cited In (53)
- Variable binding and substitution for (nameless) dummies
- Formal Reasoning Using Distributed Assertions
- Title not available (Why is that?)
- Free Theorems and Runtime Type Representations
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
- A verified framework for higher-order uncurrying optimizations
- Coq formalization of the higher-order recursive path ordering
- Directly reflective meta-programming
- Mechanized metatheory revisited
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Structural Abstract Interpretation: A Formal Study Using Coq
- Modular verification of chemical reaction network encodings via serializability analysis
- Mechanizing the Metatheory of mini-XQuery
- The Abella Interactive Theorem Prover (System Description)
- Mechanized Verification of CPS Transformations
- ASP\(_{\text{fun}}\) : a typed functional active object calculus
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Mechanizing metatheory without typing contexts
- The locally nameless representation
- POPLMark reloaded: Mechanizing proofs by logical relations
- A formalization of multi-tape Turing machines
- \(\mathrm{HO}\pi\) in Coq
- Mechanizing proofs with logical relations – Kripke-style
- Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
- Title not available (Why is that?)
- The Matita Interactive Theorem Prover
- PoplMark
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- Mechanizing type environments in weak HOAS
- Modules over monads and initial semantics
- A Rewriting Logic Approach to Type Inference
- αCheck: A mechanized metatheory model checker
- Proof assistants: history, ideas and future
- Formalizing semantic bidirectionalization and extensions with dependent types
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus
- Psi-calculi in Isabelle
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- A solution to the PoplMark challenge based on de Bruijn indices
- Formal metatheory of programming languages in the Matita interactive theorem prover
- Nominal techniques in Isabelle/HOL
- A two-level logic approach to reasoning about computations
- A list-machine benchmark for mechanized metatheory
- Nested abstract syntax in Coq
- Explicit contexts in LF (extended abstract)
- A computer-verified monadic functional implementation of the integral
- Derivation and inference of higher-order strictness types
- Nominal Inversion Principles
- Programming Inductive Proofs
- Romeo: A system for more flexible binding-safe programming
- Term-generic logic
- Formalizing Operational Semantic Specifications in Logic
- Formalizing mathematical knowledge as a biform theory graph: a case study
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Uses Software
Recommendations
- A solution to the PoplMark challenge based on de Bruijn indices 👍 👎
- Formal metatheory of programming languages in the Matita interactive theorem prover 👍 👎
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL 👍 👎
- POPLMark reloaded: Mechanizing proofs by logical relations 👍 👎
- Title not available (Why is that?) 👍 👎
This page was built for publication: Theorem Proving in Higher Order Logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5477646)
