Nominal techniques in Isabelle/HOL

DOI10.1007/s10817-008-9097-2zbMath1140.68061OpenAlexW2037026294MaRDI QIDQ928672

Publication date: 11 June 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-008-9097-2

zbMATH Keywords

Lambda-calculus Theorem provers Nominal logic work

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Formal metatheory of the lambda calculus using Stoughton's substitution, Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs, A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Game Semantics in the Nominal Model, Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL, Encoding abstract syntax without fresh names, A canonical locally named representation of binding, Formalizing adequacy: a case study for higher-order abstract syntax, A two-level logic approach to reasoning about computations, On explicit substitution with names, Algebras of UTxO blockchains, A Consistent Foundation for Isabelle/HOL, HOCore in Coq, Simple and subdirectly irreducible finitely supported \(Cb\)-sets, A Certified Functional Nominal C-Unification Algorithm, Equivariant unification, Mechanized Verification of CPS Transformations, Nominal abstraction, A formalized general theory of syntax with bindings, Unnamed Item, Rensets and renaming-based recursion for syntax with bindings extended version, Nominal AC-matching, A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols, Psi-calculi revisited: connectivity and compositionality, Proofs about Network Communication: For Humans and Machines, The locally nameless representation, A solution to the PoplMark challenge based on de Bruijn indices, Romeo: A system for more flexible binding-safe programming, Psi-calculi in Isabelle, Psi-calculi in Isabelle, Rewriting with generalized nominal unification, The Isabelle Framework, A consistent foundation for Isabelle/HOL, A formalized general theory of syntax with bindings: extended version, Binding operators for nominal sets, Completeness in PVS of a nominal unification algorithm, A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols, Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax, Structural recursion with locally scoped names, Syntactic soundness proof of a type-and-capability system with hidden state, External and internal syntax of the \(\lambda \)-calculus, Higher-order psi-calculi, Partial and nested recursive function definitions in higher-order logic, Formal SOS-Proofs for the Lambda-Calculus, Ott: Effective tool support for the working semanticist, \(\mathrm{HO}\pi\) in Coq, Proof-relevant π-calculus: a constructive account of concurrency and causality, Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets, A Simple Nominal Type Theory, Viewing \({\lambda}\)-terms through maps, Cut Elimination, Substitution and Normalisation, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, Isabelle's metalogic: formalization and proof checker, Nominal Isabelle, Mechanizing the Metatheory of mini-XQuery, Unnamed Item, Mechanized metatheory revisited, Term-generic logic, Rensets and renaming-based recursion for syntax with bindings, A formalization and proof checker for Isabelle's metalogic, Mechanizing metatheory without typing contexts, Nominal unification with letrec and environment-variables

Uses Software

Cites Work