Automated Deduction – CADE-20
From MaRDI portal
Publication:5394605
DOI10.1007/11532231zbMath1135.68561OpenAlexW2485416161MaRDI QIDQ5394605
Christine Tasson, Christian Urban
Publication date: 1 November 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11532231
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
A program logic for fresh name generation ⋮ Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations ⋮ A formalized general theory of syntax with bindings ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Implementing Spi Calculus Using Nominal Techniques ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Nominal techniques in Isabelle/HOL ⋮ The Abella Interactive Theorem Prover (System Description) ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ Nominal Inversion Principles ⋮ Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda ⋮ Generic Authenticated Data Structures, Formally. ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Alpha-structural induction and recursion for the lambda calculus in constructive type theory ⋮ Formal SOS-Proofs for the Lambda-Calculus ⋮ A Mechanized Model of the Theory of Objects ⋮ Reasoning in Abella about Structural Operational Semantics Specifications ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ Broadcast Psi-calculi with an Application to Wireless Protocols ⋮ Two-level Lambda-calculus ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ Mechanized metatheory revisited ⋮ Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
Uses Software
