Nominal lambda calculus: an internal language for FM-Cartesian closed categories

DOI10.1016/J.ENTCS.2013.09.009zbMath1334.68042OpenAlexW1986464815WikidataQ113317967 ScholiaQ113317967MaRDI QIDQ265798

Frank Nebel, Roy L. Crole

Publication date: 12 April 2016

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

zbMATH Keywords

category theorysemanticstype theorydependent typesFM-setsinternal languagenominal logic

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ A dependent type theory with abstractable names ⋮ The nominal/FM Yoneda Lemma

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• Alpha equivalence equalities
• Monads with arities and their associated theories
• A new approach to abstract syntax with variable binding
• Nominal logic, a first order theory of names and binding
• On fixpoint objects and gluing constructions
• Some lambda calculus and type theory formalized
• Nominal Lawvere theories: a category theoretic account of equational theories with names
• Nominal Sets
• Nominal Equational Logic
• The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• A dependent nominal type theory
• Adding Equations to System F Types
• Nominal Lawvere Theories
• Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
• Structural recursion with locally scoped names
• Binding in Nominal Equational Logic
• Nominal (Universal) Algebra: Equational Logic with Names and Binding
• Categories for Types
• Independence results for calculi of dependent types
• A kripke logical relation for effect-based program transformations
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES

This page was built for publication: Nominal lambda calculus: an internal language for FM-Cartesian closed categories