Daniel M Leivant - Global semantic typing for inductive and coinductive computing

lmcs:1116 - Logical Methods in Computer Science, December 25, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:18)2014
Global semantic typing for inductive and coinductive computingArticle

Authors: Daniel M Leivant

    Inductive and coinductive types are commonly construed as ontological (Church-style) types, denoting canonical data-sets such as natural numbers, lists, and streams. For various purposes, notably the study of programs in the context of global semantics, it is preferable to think of types as semantical properties (Curry-style). Intrinsic theories were introduced in the late 1990s to provide a purely logical framework for reasoning about programs and their semantic types. We extend them here to data given by any combination of inductive and coinductive definitions. This approach is of interest because it fits tightly with syntactic, semantic, and proof theoretic fundamentals of formal logic, with potential applications in implicit computational complexity as well as extraction of programs from proofs. We prove a Canonicity Theorem, showing that the global definition of program typing, via the usual (Tarskian) semantics of first-order logic, agrees with their operational semantics in the intended model. Finally, we show that every intrinsic theory is interpretable in a conservative extension of first-order arithmetic. This means that quantification over infinite data objects does not lead, on its own, to proof-theoretic strength beyond that of Peano Arithmetic. Intrinsic theories are perfectly amenable to formulas-as-types Curry-Howard morphisms, and were used to characterize major computational complexity classes Their extensions described here have similar potential which has already been applied.


    Volume: Volume 10, Issue 4
    Published on: December 25, 2014
    Imported on: December 24, 2013
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Consultation statistics

    This page has been seen 928 times.
    This article's PDF has been downloaded 583 times.