The following pages link to Nominal Isabelle (Q23989):
Displaying 50 items.
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Equivariant unification (Q616849) (← links)
- Nominal abstraction (Q617715) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Nominal unification with atom-variables (Q1640638) (← links)
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets (Q1680555) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Binding operators for nominal sets (Q1744371) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets (Q1797955) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Nominal unification with letrec and environment-variables (Q2119105) (← 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)
- Term-generic logic (Q2339466) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- Encoding abstract syntax without fresh names (Q2392477) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- Formalizing adequacy: a case study for higher-order abstract syntax (Q2392483) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- On explicit substitution with names (Q2392486) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- A simple nominal type theory (Q2804939) (← links)
- Reasoning in Abella about structural operational semantics specifications (Q2804943) (← links)
- Formalizing Cut Elimination of Coalgebraic Logics in Coq (Q2851950) (← links)
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking (Q2871867) (← links)
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (Q2891399) (← links)
- Mechanizing the metatheory of LF (Q2946633) (← links)
- Psi-calculi: a framework for mobile processes with nominal data and logic (Q3003314) (← 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)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- Game Semantics in the Nominal Model (Q3178282) (← links)
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL (Q3183537) (← links)
