A dependent type theory with abstractable names

DOI10.1016/J.ENTCS.2015.04.003zbMath1342.68054OpenAlexW2053194822WikidataQ113317811 ScholiaQ113317811MaRDI QIDQ530845

Justus Matthiesen, Jasper Derikx, Andrew M. Pitts

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)

Related Items (7)

Nominal essential intersection types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Dependent Types and Fibred Computational Effects ⋮ Modal dependent type theory and dependent right adjoints ⋮ Unnamed Item

Uses Software

• Freshml
• FreshOCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• Generalized algebraic theories and contextual categories
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Nominal Sets
• Nominal Equational Logic
• Nominal Coalgebraic Data Types with Applications to Lambda Calculus
• A dependent nominal type theory
• Nominal (Universal) Algebra: Equational Logic with Names and Binding
• A framework for defining logics
• Internal type theory
• FreshML
• Computer Science Logic
• Homotopy Type Theory: Univalent Foundations of Mathematics

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