Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477646
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
- scientific article; zbMATH DE number 7204440
Cited in
(54)- Variable binding and substitution for (nameless) dummies
- Romeo: a system for more flexible binding-safe programming
- Formal Reasoning Using Distributed Assertions
- scientific article; zbMATH DE number 7809762 (Why is no real title available?)
- Proof assistants: history, ideas and future
- Formalizing operational semantic specifications in logic
- Modules over monads and initial semantics
- Mechanizing metatheory without typing contexts
- Programming inductive proofs. A new approach based on contextual types
- The locally nameless representation
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Mechanizing the metatheory of mini-XQuery
- Psi-calculi in Isabelle
- ASP\(_{\text{fun}}\) : a typed functional active object calculus
- A two-level logic approach to reasoning about computations
- Nested abstract syntax in Coq
- POPLMark reloaded: mechanizing proofs by logical relations
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Modular verification of chemical reaction network encodings via serializability analysis
- Nominal Inversion Principles
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- A Rewriting Logic Approach to Type Inference
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A list-machine benchmark for mechanized metatheory
- \(\mathrm{HO}\pi\) in Coq
- Formalizing semantic bidirectionalization and extensions with dependent types
- 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
- The Matita interactive theorem prover
- A higher-order abstract syntax approach to verified transformations on functional programs
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- A formalization of multi-tape Turing machines
- Mechanizing type environments in weak HOAS
- PoplMark
- αCheck: A mechanized metatheory model checker
- Term-generic logic
- The Abella Interactive Theorem Prover (System Description)
- A verified framework for higher-order uncurrying optimizations
- Mechanizing proofs with logical relations -- Kripke-style
- Mechanized metatheory revisited
- Coq formalization of the higher-order recursive path ordering
- Derivation and inference of higher-order strictness types
- Directly reflective meta-programming
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Mechanized Verification of CPS Transformations
- Structural Abstract Interpretation: A Formal Study Using Coq
- Formalizing mathematical knowledge as a biform theory graph: a case study
- Explicit contexts in LF (extended abstract)
- Free theorems and runtime type representations
- Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
- A list-machine benchmark for mechanized metatheory (extended abstract)
- A computer-verified monadic functional implementation of the integral
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)
