Nominal Isabelle
From MaRDI portal
swMATH12055MaRDI QIDQ23989FDOQ23989
Author name not available (Why is that?)
Official website: https://isabelle.in.tum.de/nominal/
Cited In (only showing first 100 items - show all)
- Rensets and renaming-based recursion for syntax with bindings
- 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
- Formalizing cut elimination of coalgebraic logics in Coq
- Generic Authenticated Data Structures, Formally.
- Mechanizing metatheory without typing contexts
- Robinson arithmetic
- Mechanizing the metatheory of LF
- Algebras of UTxO blockchains
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- \(\mathrm{HO}\pi\) in Coq
- Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
- A program logic for fresh name generation
- Romeo: a system for more flexible binding-safe programming
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Game semantics in the nominal model
- αCheck: A mechanized metatheory model checker
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets
- Encoding abstract syntax without fresh names
- Formal SOS-Proofs for the Lambda-Calculus
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- A solution to the PoplMark challenge based on de Bruijn indices
- The language of stratified sets is confluent and strongly normalising
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Cut elimination, substitution and normalisation
- Nominal Inversion Principles
- Nominal Unification and Matching of Higher Order Expressions with Recursive Let
- Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
- Mechanizing the metatheory of mini-XQuery
- Rewriting with generalized nominal unification
- Viewing \({\lambda}\)-terms through maps
- 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
- A formalized general theory of syntax with bindings: extended version
- Nominal abstraction
- The locally nameless representation
- General bindings and alpha-equivalence in Nominal Isabelle
- Psi-calculi in Isabelle
- Nominal unification with atom-variables
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- A canonical locally named representation of binding
- Nominal unification with atom and context variables
- Broadcast psi-calculi with an application to wireless protocols
- External and internal syntax of the \(\lambda \)-calculus
- Equivariant unification
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- HYBRID
- Beluga
- Twelf
- Teaching semantics with a proof assistant: no more LSD trip proofs
- AURA
- CloneDigger
- Abella
- Bedwyr
- LEGO
- aleanTAP
- SCC
- Fudgets
- Gmeta
- LNgen
- PoplMark
- Jitawa
- CC-Pi
- A learning-based fact selector for Isabelle/HOL
- 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
- A simple nominal type theory
This page was built for software: Nominal Isabelle
