The following pages link to Automated Deduction – CADE-20 (Q5394605):
Displaying 31 items.
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- A program logic for fresh name generation (Q2145263) (← links)
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda (Q2229159) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Reasoning in Abella about structural operational semantics specifications (Q2804943) (← links)
- Isabelle/UTP: A Mechanised Theory Engineering Framework (Q2814613) (← links)
- Nominal reasoning techniques in Coq (extended abstract) (Q2871861) (← links)
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking (Q2871867) (← links)
- Broadcast Psi-calculi with an Application to Wireless Protocols (Q3095234) (← links)
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem (Q3100205) (← links)
- Implementing Spi Calculus Using Nominal Techniques (Q3507444) (← links)
- The Abella Interactive Theorem Prover (System Description) (Q3541698) (← links)
- A Compiled Implementation of Normalization by Evaluation (Q3543648) (← links)
- Nominal Inversion Principles (Q3543650) (← links)
- Two-level Lambda-calculus (Q4982628) (← links)
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention (Q5022932) (← links)
- Equivariant ZFA and the foundations of nominal techniques (Q5112646) (← links)
- Formal SOS-Proofs for the Lambda-Calculus (Q5178966) (← links)
- A Mechanized Model of the Theory of Objects (Q5428912) (← links)
- Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle (Q5505488) (← links)
- Generic Authenticated Data Structures, Formally. (Q5875417) (← links)
- General bindings and alpha-equivalence in Nominal Isabelle (Q5891628) (← links)
- General Bindings and Alpha-Equivalence in Nominal Isabelle (Q5892493) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
