 |
 |
James Cheney - A dependent nominal type theory
lmcs:1042 - Logical Methods in Computer Science, February 20, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:8)2012A dependent nominal type theoryArticle
Authors: James Cheney 
Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. We present a LF-style dependent type theory extended with name-abstraction types, prove soundness and decidability of beta-eta-equivalence checking, discuss adequacy and canonical forms via an example, and discuss extensions such as dependently-typed recursion and induction principles.
Source: arXiv.org:1201.5240
Volume: Volume 8, Issue 1
Secondary volumes: Special Issue on Types for Proofs and Programs
Published on: February 20, 2012
Imported on: May 12, 2011
Keywords: Computer Science - Logic in Computer Science, Computer Science - Programming Languages, F.4.1
Classifications
Mathematics Subject Classification 20201
- 03B30 - Foundations of classical theories (including reverse mathematics)
- 03F20 - Complexity of proofs
- 15A15 - Determinants, permanents, traces, other special matrix functions
- 15B33 - Matrices over special rings (quaternions, finite fields, etc.)
- 68Q15 - Complexity classes (hierarchies, relations among complexity classes, etc.)
12 Documents citing this article
Consultation statistics
This page has been seen 3370 times.
This article's PDF has been downloaded 603 times.