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)2012
A dependent nominal type theory

Authors: James Cheney ORCID-iD

    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.


    Volume: Volume 8, Issue 1
    Published on: February 20, 2012
    Accepted on: June 25, 2015
    Submitted on: May 12, 2011
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.4.1

    Linked data

    Source : ScholeXplorer References DOI 10.1145/1577824.1577836
    • 10.1145/1577824.1577836
    an intensional approach to encoding name-bindings
    Evan Austin ; Edwin Westbrook ; Aaron Stump ;

    11 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 438 times.
    This article's PDF has been downloaded 240 times.