Output details
11 - Computer Science and Informatics
University of Leicester
Output title
Nominal Lambda Calculus: An Internal Language for FM-Cartesian Closed Categories
Type
E - Conference contribution
Name of conference/published proceedings
Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIX. ENTCS volume 298.
Volume number
298
Issue number
-
First page of article
93
ISSN of proceedings
15710661
Year of publication
2013
URL
-
Number of additional authors
1
Additional information
<10> Central to nominal computation theory are abstraction and partial concretion operations, from which useful notions of local scoping may be defined. That concretion is partial is known to be a hindrance in practical applications: we neatly solve this problem of partiality by developing a novel dependently typed equational system, called Nominal Lambda Calculus. This is the first sound and complete combination of abstraction, concretion and higher order functions and paves the way for applications in theorem proving. (This work was presented at MFPS XXIX, USA, 2013.)
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
-
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
