The following pages link to Nominal techniques in Isabelle/HOL (Q928672):
Displaying 50 items.
- Nominal Isabelle (Q23989) (← links)
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Equivariant unification (Q616849) (← links)
- Nominal abstraction (Q617715) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets (Q1680555) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← 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)
- 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 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)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← 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)
- 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)
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (Q2891399) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- HOCore in Coq (Q2945640) (← links)
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax (Q3011103) (← links)
- Structural recursion with locally scoped names (Q3016213) (← 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)
- Mechanized Verification of CPS Transformations (Q3498467) (← links)
- The Isabelle Framework (Q3543647) (← links)
- Proof-relevant π-calculus: a constructive account of concurrency and causality (Q4691184) (← links)
- Syntactic soundness proof of a type-and-capability system with hidden state (Q4912884) (← links)
- (Q4993360) (← links)
- Algebras of UTxO blockchains (Q5084313) (← links)
- A Certified Functional Nominal C-Unification Algorithm (Q5097631) (← links)
- Rewriting with generalized nominal unification (Q5139280) (← links)
