Nominal Isabelle
From MaRDI portal
Cited in
(only showing first 100 items - show all)- HYBRID
- Ott
- metalib
- Beluga
- Isabelle/HOL
- Nominal unification with atom-variables
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets
- A consistent foundation for Isabelle/HOL
- Binding operators for nominal sets
- Completeness in PVS of a nominal unification algorithm
- 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
- Free functor from the category of G-nominal sets to that of 01-G-nominal sets
- Twelf
- The locally nameless representation
- 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 formalized general theory of syntax with bindings: extended version
- \(\mathrm{HO}\pi\) in Coq
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- CloneDigger
- FreshML
- Rensets and renaming-based recursion for syntax with bindings
- A formalization and proof checker for Isabelle's metalogic
- Nominal unification with letrec and environment-variables
- Bedwyr
- Abella
- A program logic for fresh name generation
- LEGO
- SCC
- aleanTAP
- Fudgets
- PoplMark
- Gmeta
- LNgen
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
- Mechanized metatheory revisited
- Term-generic logic
- AURA
- Mechanizing metatheory without typing contexts
- Formal metatheory of the lambda calculus using Stoughton's substitution
- 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
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Jitawa
- CC-Pi
- A simple nominal type theory
- Reasoning in Abella about structural operational semantics specifications
- Formalizing cut elimination of coalgebraic logics in Coq
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
- Teaching semantics with a proof assistant: no more LSD trip proofs
- Mechanizing the metatheory of LF
- Psi-calculi: a framework for mobile processes with nominal data and logic
- Broadcast psi-calculi with an application to wireless protocols
- Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
- Mechanizing the metatheory of mini-XQuery
- Game semantics in the nominal model
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- MiniAgda
- A learning-based fact selector for Isabelle/HOL
- Elf
- Teyjus
- Delphin
- CLF
- Unbound
- FreshOCaml
- CoCaml
- Autosubst
- mini-ML
- CRSX
- The Isabelle Framework
- A Compiled Implementation of Normalization by Evaluation
- Nominal Inversion Principles
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Nettle
- FinFuns
- Depth First Search
- Psi-calculi
- Tame Graphs
- Jinja not Java
- Light-weight Containers
- Launchbury
- DrACuLa
- ACUOS2
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Call_Arity
- The adequacy of Launchbury's natural semantics for lazy evaluation
- αCheck: A mechanized metatheory model checker
- The language of stratified sets is confluent and strongly normalising
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- Mechanizing proofs with logical relations -- Kripke-style
- Two-level lambda-calculus
- Nominal unification with atom and context variables
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Nominal Unification and Matching of Higher Order Expressions with Recursive Let
- Algebras of UTxO blockchains
This page was built for software: Nominal Isabelle
