A dependent type theory with abstractable names

DOI10.1016/J.ENTCS.2015.04.003MaRDI QIDQ530845zbMATH OpenOpenAlexWikidataFDO

Authors Andrew M. Pitts, Justus Matthiesen, Jasper Derikx

Publication date 1 August 2016

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

zbMATH Keywords

dependent typesbindingnominal setsnames

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• A dependent nominal type theory
• Computer Science Logic
• A simple nominal type theory
• Dependent types for nominal terms with atom substitutions
• scientific article; zbMATH DE number 1241699

Cites work

• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• A dependent nominal type theory
• A framework for defining logics
• Computer Science Logic
• FreshML: programming with binders made simple
• Generalized algebraic theories and contextual categories
• Homotopy type theory. Univalent foundations of mathematics
• Internal type theory
• Nominal (universal) algebra: equational logic with names and binding
• Nominal coalgebraic data types with applications to lambda calculus
• Nominal equational logic
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• Nominal logic, a first order theory of names and binding
• Nominal sets. Names and symmetry in computer science
• Nominal unification

Cited in

(12)

• A dependent nominal type theory
• Modal dependent type theory and dependent right adjoints
• scientific article; zbMATH DE number 7288622 (Why is no real title available?)
• Transpension: the right adjoint to the Pi-type
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Dependent types for nominal terms with atom substitutions
• Computer Science Logic
• The clocks they are adjunctions. Denotational semantics for clocked type theory
• A simple nominal type theory
• Nominal essential intersection types
• Validating Brouwer's continuity principle for numbers using named exceptions
• Dependent types and fibred computational effects

Describes a project that uses

Uses Software

• FreshML
• FreshOCaml

This page was built for publication: A dependent type theory with abstractable names

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