A dependent nominal type theory

DOI10.2168/LMCS-8(1:8)2012MaRDI QIDQ2881075zbMATH OpenFDO

Authors James Cheney

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1201.5240

zbMATH Keywords

dependent typesnominal abstract syntax

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Abstract: Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. We present a LF-style dependent type theory extended with name-abstraction types, prove soundness and decidability of beta-eta-equivalence checking, discuss adequacy and canonical forms via an example, and discuss extensions such as dependently-typed recursion and induction principles.

Recommendations

• A dependent type theory with abstractable names
• A simple nominal type theory
• Computer Science Logic
• Dependent types for nominal terms with atom substitutions
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax

Cited in

(11)

• Nominal essential intersection types
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• A simple nominal type theory
• On generically stable types in dependent theories
• Validating Brouwer's continuity principle for numbers using named exceptions
• scientific article; zbMATH DE number 2087549 (Why is no real title available?)
• Internal parametricity for cubical type theory
• Dependent types for nominal terms with atom substitutions
• A dependent type theory with abstractable names
• Computer Science Logic
• Transpension: the right adjoint to the Pi-type

Describes a project that uses

Uses Software

• FreshML

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

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