A dependent type theory with abstractable names

DOI10.1016/J.ENTCS.2015.04.003zbMATH Open1342.68054OpenAlexW2053194822WikidataQ113317811 ScholiaQ113317811MaRDI QIDQ530845FDOQ530845

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

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

zbMATH Keywords

dependent typesbindingnominal setsnames

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (12)

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

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)