Cited in
(only showing first 100 items - show all)- Automated Deduction – CADE-20
- External and internal syntax of the \(\lambda \)-calculus
- A formalized general theory of syntax with bindings: extended version
- On explicit substitution with names
- A consistent foundation for Isabelle/HOL
- The locally nameless representation
- Psi-calculi: a framework for mobile processes with nominal data and logic
- Teaching semantics with a proof assistant: no more LSD trip proofs
- Psi-calculi in Isabelle
- Nominal unification with atom and context variables
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Broadcast psi-calculi with an application to wireless protocols
- A two-level logic approach to reasoning about computations
- POPLMark reloaded: mechanizing proofs by logical relations
- Viewing \({\lambda}\)-terms through maps
- A Mechanized Model of the Theory of Objects
- Modal logics for nominal transition systems
- Two-level lambda-calculus
- Rewriting with generalized nominal unification
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A new foundation for Nominal Isabelle
- General bindings and alpha-equivalence in Nominal Isabelle
- Psi-calculi in Isabelle
- Equivariant unification
- Formalizing adequacy: a case study for higher-order abstract syntax
- Nominal abstraction
- HYBRID
- Ott
- Beluga
- Isabelle/HOL
- Twelf
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- AURA
- CloneDigger
- Abella
- Bedwyr
- LEGO
- aleanTAP
- SCC
- Fudgets
- Gmeta
- LNgen
- PoplMark
- Jitawa
- CC-Pi
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets
- FreshML
- CLF
- Delphin
- Elf
- MiniAgda
- Teyjus
- Autosubst
- CoCaml
- FreshOCaml
- mini-ML
- CRSX
- Unbound
- Nettle
- Depth First Search
- FinFuns
- Psi-calculi
- Jinja not Java
- Light-weight Containers
- Launchbury
- Tame Graphs
- DrACuLa
- ACUOS2
- Call_Arity
- Term-generic logic
- Mechanizing proofs with logical relations -- Kripke-style
- Mechanized metatheory revisited
- A formalization and proof checker for Isabelle's metalogic
- Binding operators for nominal sets
- Completeness in PVS of a nominal unification algorithm
- metalib
- A Compiled Implementation of Normalization by Evaluation
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- A learning-based fact selector for Isabelle/HOL
- The adequacy of Launchbury's natural semantics for lazy evaluation
- A canonical locally named representation of binding
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Reasoning in Abella about structural operational semantics specifications
- Partial and nested recursive function definitions in higher-order logic
- A simple nominal type theory
- Nominal unification with atom-variables
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- The Isabelle Framework
- Algebras of UTxO blockchains
- Mechanizing metatheory without typing contexts
- Game semantics in the nominal model
- Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
- Mechanizing the metatheory of mini-XQuery
- Romeo: a system for more flexible binding-safe programming
- Formalizing cut elimination of coalgebraic logics in Coq
- Mechanizing the metatheory of LF
- Nominal Inversion Principles
- Formal SOS-Proofs for the Lambda-Calculus
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Robinson arithmetic
This page was built for software: Nominal Isabelle
