A simple nominal type theory

DOI10.1016/J.ENTCS.2008.12.115MaRDI QIDQ2804939zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• A dependent nominal type theory
• A simple sequent calculus for nominal logic
• A dependent type theory with abstractable names
• Nominal logic, a first order theory of names and binding
• scientific article; zbMATH DE number 2242589

Cites work

• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• A new approach to abstract syntax with variable binding
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Alpha-structural recursion and induction
• Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
• Completeness and Herbrand theorems for nominal logic
• Computer Science Logic
• Consistency of the theory of contexts
• Foundations of Software Science and Computational Structures
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• Nominal logic, a first order theory of names and binding
• Nominal techniques in Isabelle/HOL
• Nominal unification
• On bunched typing
• Practical Programming with Higher-Order Encodings and Dependent Types
• Primitive recursion for higher-order abstract syntax
• Theorem Proving in Higher Order Logics
• Typed Lambda Calculi and Applications

Cited in

(15)

• Curry-Style Types for Nominal Terms
• Nominalistic logic: from naive set theory to intensional type theory
• A dependent nominal type theory
• A simple sequent calculus for nominal logic
• Abstract clones for abstract syntax
• Nominal abstraction
• Foundations of Software Science and Computational Structures
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Dependent types for nominal terms with atom substitutions
• Permissive-nominal logic: first-order logic over nominal terms and sets
• A dependent type theory with abstractable names
• Nominal essential intersection types
• Validating Brouwer's continuity principle for numbers using named exceptions
• Simply-typed underdeterminism
• Principal types for nominal theories

Describes a project that uses

Uses Software

• FreshML
• Nominal Isabelle

This page was built for publication: A simple nominal type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804939)