Mechanized metatheory revisited
From MaRDI portal
Publication:2323447
Recommendations
- Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
- A formalized general theory of syntax with bindings: extended version
- GMeta: a generic formal metatheory framework for first-order representations
- Engineering formal metatheory
- A formalized general theory of syntax with bindings
Cites work
- -calculus in (Co)inductive-type theory
- \(\pi\)-calculus, internal mobility, and agent-passing calculi
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A Brief Overview of Mizar
- A calculus of mobile processes. I
- A calculus of mobile processes. II
- A case study in programming coinductive proofs: Howe's method
- A characterisation of open bisimilarity using an intuitionistic modal logic
- A compact representation of proofs
- A framework for defining logics
- A higher-order abstract syntax approach to verified transformations on functional programs
- A logic for reasoning about generic judgments
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A new approach to abstract syntax with variable binding
- A notation for lambda terms. A generalization of environments
- A proof of cut-elimination theorem in simple type-theory
- A proof theory for generic judgments
- A structural approach to operational semantics
- A two-level logic approach to reasoning about computations
- A two-level logic approach to reasoning about typed specification languages
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Abella: a system for reasoning about relational specifications
- Alpha-structural recursion and induction
- An introduction to mathematical logic and type theory: To truth through proof.
- Automated Deduction – CADE-20
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Checking NFA equivalence with bisimulations up to congruence
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Complete Lattices and Up-To Techniques
- Computer Science Logic
- CONCUR 2005 – Concurrency Theory
- Contextual modal type theory
- Cut elimination for a logic with induction and co-induction
- Cut-elimination for a logic with definitions and induction
- Edinburgh LCF. A mechanized logic of computation
- ELPI: fast, embeddable, Prolog interpreter
- Engineering formal metatheory
- Enhancements of the bisimulation proof method
- From operational semantics to abstract machines
- Hauptsatz for higher order logic
- HOCore in Coq
- HOL Light: An Overview
- scientific article; zbMATH DE number 1612495 (Why is no real title available?)
- scientific article; zbMATH DE number 1701361 (Why is no real title available?)
- scientific article; zbMATH DE number 2185657 (Why is no real title available?)
- scientific article; zbMATH DE number 2127501 (Why is no real title available?)
- scientific article; zbMATH DE number 4180832 (Why is no real title available?)
- scientific article; zbMATH DE number 4164201 (Why is no real title available?)
- scientific article; zbMATH DE number 3988745 (Why is no real title available?)
- scientific article; zbMATH DE number 4035108 (Why is no real title available?)
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 1303348 (Why is no real title available?)
- scientific article; zbMATH DE number 1348473 (Why is no real title available?)
- scientific article; zbMATH DE number 512769 (Why is no real title available?)
- scientific article; zbMATH DE number 1158760 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- scientific article; zbMATH DE number 7015113 (Why is no real title available?)
- scientific article; zbMATH DE number 2174396 (Why is no real title available?)
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Introduction to generalized type systems
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Kripke-style models for typed lambda calculus
- Logic Programming
- Mechanizing the metatheory of LF
- Modal logics for mobile processes
- Natural deduction as higher-order resolution
- Nominal abstraction
- Nominal logic, a first order theory of names and binding
- Nominal techniques in Isabelle/HOL
- On the expressivity of minimal generic quantification
- Ott: Effective tool support for the working semanticist
- Parametric higher-order abstract syntax for mechanized semantics
- Polymorphic lemmas and definitions in \lambdaProlog and Twelf
- Program extraction from normalization proofs
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
- Provability in Elementary Type Theory
- Proving and applying program transformations expressed with second-order patterns
- Proving congruence of bisimulation in functional programming languages
- Reasoning with higher-order abstract syntax in a logical framework
- Resolution in type theory
- Separating functional computation from relations
- SPEC: an equivalence checker for security protocols
- The -calculus: A theory of mobile processes
- The Abella Interactive Theorem Prover (System Description)
- The calculus of constructions
- The lambda calculus is algebraic
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- The undecidability of unification in third order logic
- Theorem Proving in Higher Order Logics
- Type inference for polymorphic references
- Unification under a mixed prefix
- Uniform proofs as a foundation for logic programming
- Weak Bisimulation Up to Elaboration
Cited in
(8)- Knowledge, machines, and the consistency of Reinhardt's strong mechanistic thesis
- GMeta: a generic formal metatheory framework for first-order representations
- Mechanizing the metatheory of LF
- Mechanizing metatheory in a logical framework
- Theorem Proving in Higher Order Logics
- Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Two applications of logic programming to Coq
Describes a project that uses
Uses Software
This page was built for publication: Mechanized metatheory revisited
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2323447)
