Mechanized metatheory revisited
From MaRDI portal
Publication:2323447
DOI10.1007/s10817-018-9483-3zbMath1468.68303OpenAlexW2895763214MaRDI QIDQ2323447
Publication date: 2 September 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01884210/file/paper.pdf
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Reasoning with higher-order abstract syntax in a logical framework
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Weak Bisimulation Up to Elaboration
- Least and Greatest Fixed Points in Linear Logic
- CONCUR 2005 – Concurrency Theory
- 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
- 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
- Nominal abstraction
- \(\pi\)-calculus, internal mobility, and agent-passing calculi
- Modal logics for mobile processes
- A new approach to abstract syntax with variable binding
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Kripke-style models for typed lambda calculus
- Program extraction from normalization proofs
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Type inference for polymorphic references
- Nominal techniques in Isabelle/HOL
- A compact representation of proofs
- The calculus of constructions
- A notation for lambda terms. A generalization of environments
- A calculus of mobile processes. I
- A calculus of mobile processes. II
- Unification under a mixed prefix
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Proving and applying program transformations expressed with second-order patterns
- Isabelle. A generic theorem prover
- Cut-elimination for a logic with definitions and induction
- \(\pi\)-calculus in (Co)inductive-type theory
- Isabelle/HOL. A proof assistant for higher-order logic
- Edinburgh LCF. A mechanized logic of computation
- An introduction to mathematical logic and type theory: To truth through proof.
- A structural approach to operational semantics
- Nominal logic, a first order theory of names and binding
- Proving congruence of bisimulation in functional programming languages
- Cut elimination for a logic with induction and co-induction
- A two-level logic approach to reasoning about computations
- A proof of cut-elimination theorem in simple type-theory
- Uniform proofs as a foundation for logic programming
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
- On the Expressivity of Minimal Generic Quantification
- Checking NFA equivalence with bisimulations up to congruence
- HOCore in Coq
- Proof search specifications of bisimulation and modal logics for the π-calculus
- Mechanizing the metatheory of LF
- A Two-Level Logic Approach to Reasoning about Typed Specification Languages
- SPEC: An Equivalence Checker for Security Protocols
- HOL Light: An Overview
- A Brief Overview of Mizar
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Engineering formal metatheory
- ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
- Complete Lattices and Up-To Techniques
- The Abella Interactive Theorem Prover (System Description)
- Alpha-structural recursion and induction
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A framework for defining logics
- Provability in Elementary Type Theory
- From operational semantics to abstract machines
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- The lambda calculus is algebraic
- Natural deduction as higher-order resolution
- Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property
- Introduction to generalized type systems
- Divergence and unique solution of equations
- Parametric higher-order abstract syntax for mechanized semantics
- Ott: Effective tool support for the working semanticist
- Abella: A System for Reasoning about Relational Specifications
- A case study in programming coinductive proofs: Howe’s method
- A proof theory for generic judgments
- Contextual modal type theory
- Computer Science Logic
- Logic Programming
- Automated Deduction – CADE-20
- Enhancements of the bisimulation proof method
- Theorem Proving in Higher Order Logics
- Hauptsatz for higher order logic
- Resolution in type theory
- The undecidability of unification in third order logic
This page was built for publication: Mechanized metatheory revisited
