Cited in
(only showing first 100 items - show all)- A two-level logic approach to reasoning about computations
- Psi-calculi: a framework for mobile processes with nominal data and logic
- metalib
- POPLMark reloaded: mechanizing proofs by logical relations
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
- The language of stratified sets is confluent and strongly normalising
- A Compiled Implementation of Normalization by Evaluation
- 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
- Mechanizing proofs with logical relations -- Kripke-style
- Cut elimination, substitution and normalisation
- Nominal Inversion Principles
- Two-level lambda-calculus
- Nominal Unification and Matching of Higher Order Expressions with Recursive Let
- Term-generic logic
- Modal logics for nominal transition systems
- Robinson arithmetic
- A consistent foundation for Isabelle/HOL
- Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
- Mechanizing the metatheory of mini-XQuery
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Reasoning in Abella about structural operational semantics specifications
- A new foundation for Nominal Isabelle
- Rensets and renaming-based recursion for syntax with bindings
- Rewriting with generalized nominal unification
- 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
- 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
- Mechanized metatheory revisited
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Formalizing cut elimination of coalgebraic logics in Coq
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Generic Authenticated Data Structures, Formally.
- The Isabelle Framework
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Automated Deduction – CADE-20
- A Mechanized Model of the Theory of Objects
- A formalized general theory of syntax with bindings: extended version
- Mechanizing metatheory without typing contexts
- Nominal abstraction
- The adequacy of Launchbury's natural semantics for lazy evaluation
- The locally nameless representation
- Mechanizing the metatheory of LF
- Nominal unification with atom-variables
- General bindings and alpha-equivalence in Nominal Isabelle
- Psi-calculi in Isabelle
- \(\mathrm{HO}\pi\) in Coq
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Algebras of UTxO blockchains
- A canonical locally named representation of binding
- A program logic for fresh name generation
- Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
- Broadcast psi-calculi with an application to wireless protocols
- Nominal unification with atom and context variables
- Romeo: a system for more flexible binding-safe programming
- External and internal syntax of the \(\lambda \)-calculus
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Equivariant unification
- HYBRID
- Ott
- Beluga
- Isabelle/HOL
- Twelf
- AURA
- CloneDigger
- Abella
- Bedwyr
- LEGO
- aleanTAP
- SCC
- Fudgets
- Gmeta
- LNgen
- PoplMark
- Jitawa
- CC-Pi
- 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
This page was built for software: Nominal Isabelle
