A Simple Nominal Type Theory

DOI10.1016/j.entcs.2008.12.115zbMath1337.03039OpenAlexW2141444450MaRDI QIDQ2804939

James Cheney

Publication date: 6 May 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.115

zbMATH Keywords

type systemsnominal terms

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Nominal essential intersection types ⋮ Validating Brouwer's continuity principle for numbers using named exceptions

Uses Software

• Freshml
• Nominal Isabelle

Cites Work

• Unnamed Item
• A new approach to abstract syntax with variable binding
• Nominal techniques in Isabelle/HOL
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Alpha-structural recursion and induction
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• On bunched typing
• Boxes go bananas
• Computer Science Logic
• Practical Programming with Higher-Order Encodings and Dependent Types
• Theorem Proving in Higher Order Logics
• Consistency of the theory of contexts
• Completeness and Herbrand theorems for nominal logic
• Typed Lambda Calculi and Applications
• Foundations of Software Science and Computational Structures
• Primitive recursion for higher-order abstract syntax

This page was built for publication: A Simple Nominal Type Theory