Nominal Isabelle
From MaRDI portal
Software:23989
swMATH12055MaRDI QIDQ23989FDOQ23989
Author name not available (Why is that?)
Cited In (78)
- Rensets and renaming-based recursion for syntax with bindings
- Rewriting with generalized nominal unification
- Title not available (Why is that?)
- Viewing \({\lambda}\)-terms through maps
- Nominal unification with letrec and environment-variables
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Mechanized metatheory revisited
- Binding operators for nominal sets
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Completeness in PVS of a nominal unification algorithm
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- The Isabelle Framework
- Automated Deduction – CADE-20
- A Mechanized Model of the Theory of Objects
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- The adequacy of Launchbury's natural semantics for lazy evaluation
- Mechanizing metatheory without typing contexts
- A formalized general theory of syntax with bindings: extended version
- Nominal abstraction
- The locally nameless representation
- POPLMark reloaded: Mechanizing proofs by logical relations
- Mechanizing the metatheory of LF
- General bindings and alpha-equivalence in Nominal Isabelle
- Psi-calculi in Isabelle
- Nominal unification with atom-variables
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- \(\mathrm{HO}\pi\) in Coq
- Mechanizing proofs with logical relations – Kripke-style
- A canonical locally named representation of binding
- A program logic for fresh name generation
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Two-level Lambda-calculus
- Formalizing Cut Elimination of Coalgebraic Logics in Coq
- External and internal syntax of the \(\lambda \)-calculus
- Equivariant unification
- Cut Elimination, Substitution and Normalisation
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Title not available (Why is that?)
- A learning-based fact selector for Isabelle/HOL
- A simple nominal type theory
- αCheck: A mechanized metatheory model checker
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets
- On explicit substitution with names
- Formalizing adequacy: a case study for higher-order abstract syntax
- Encoding abstract syntax without fresh names
- A formalization and proof checker for Isabelle's metalogic
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets
- Psi-calculi in Isabelle
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- A solution to the PoplMark challenge based on de Bruijn indices
- A New Foundation for Nominal Isabelle
- Psi-calculi: a framework for mobile processes with nominal data and logic
- A two-level logic approach to reasoning about computations
- Broadcast Psi-calculi with an Application to Wireless Protocols
- A Compiled Implementation of Normalization by Evaluation
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
- Partial and nested recursive function definitions in higher-order logic
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Term-generic logic
- Proof-relevant π-calculus: a constructive account of concurrency and causality
- A consistent foundation for Isabelle/HOL
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Reasoning in Abella about structural operational semantics specifications
- Generic Authenticated Data Structures, Formally.
- Mechanizing the Metatheory of mini-XQuery
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
- Algebras of UTxO blockchains
- Title not available (Why is that?)
- Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
- Formal SOS-Proofs for the Lambda-Calculus
- Game Semantics in the Nominal Model
- Nominal Inversion Principles
- Nominal Unification and Matching of Higher Order Expressions with Recursive Let
- Romeo: A system for more flexible binding-safe programming
This page was built for software: Nominal Isabelle
