A simple nominal type theory

DOI10.1016/J.ENTCS.2008.12.115zbMATH Open1337.03039OpenAlexW2141444450MaRDI QIDQ2804939FDOQ2804939

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

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

zbMATH Keywords

type systemsnominal terms

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (15)

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

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)