Nominal lambda calculus: an internal language for FM-Cartesian closed categories
type: Item
instance of: scholarly article
title: Nominal lambda calculus: an internal language for FM-Cartesian closed categories
zbMATH Open document ID: 1334.68042
author: Roy L. Crole
author: Frank Nebel
publication date: 2016-04-12T00:00:00Z
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 18D15
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 6567556
zbMATH Keywords: category theory
zbMATH Keywords: dependent types
zbMATH Keywords: FM-sets
zbMATH Keywords: internal language
zbMATH Keywords: nominal logic
zbMATH Keywords: semantics
zbMATH Keywords: type theory
MaRDI profile type: Publication
full work available at URL: j.entcs.2013.09.009
OpenAlex ID: W1986464815
Wikidata QID: Q113317967
cites work: Monads with arities and their associated theories
cites work: A dependent nominal type theory
cites work: Binding in Nominal Equational Logic
cites work: Nominal Lawvere Theories
cites work: Nominal Lawvere theories: a category theoretic account of equational theories with names
cites work: Nominal equational logic
cites work: On fixpoint objects and gluing constructions
cites work: Categories for Types
cites work: Alpha equivalence equalities
cites work: Q3995720
cites work: A new approach to abstract syntax with variable binding
cites work: Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
cites work: Nominal (Universal) Algebra: Equational Logic with Names and Binding
cites work: Q4722037
cites work: The category theoretic understanding of universal algebra: Lawvere theories and monads
cites work: Adding Equations to System F Types
cites work: Q3727946
cites work: FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
cites work: Q4123496
cites work: Some lambda calculus and type theory formalized
cites work: Q3999860
cites work: Nominal logic, a first order theory of names and binding
cites work: Structural recursion with locally scoped names
cites work: Nominal sets. Names and symmetry in computer science
cites work: Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
cites work: Independence results for calculi of dependent types
cites work: Q5286647
cites work: A kripke logical relation for effect-based program transformations
DOI: 10.1016/J.ENTCS.2013.09.009
Recommended article: Q3749213
Recommended article: Q3760508
Recommended article: Q3827990
Recommended article: A Nominal Axiomatization of the Lambda Calculus
Recommended article: Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category
Recommended article: Categorical semantics for higher order polymorphic lambda calculus
Recommended article: Q4896529
Recommended article: The maximality of the typed lambda calculus and of cartesian closed categories
Recommended article: Q5150148
Recommended article: A Concrete Categorical Model for the Lambek Syntactic Calculus
description: scientific article; zbMATH DE number 6567556