Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille

Preprint English OPEN
Jenkins, Christopher; McDonald, Colin; Stump, Aaron;
(2019)
  • Subject: Computer Science - Programming Languages | 68N15
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES | TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS

In CDLE, a pure Curry-style type theory, it is possible to generically derive induction for lambda-encoded data whose types are least fixed points of functors. From this comes fruitful research into the design-space for datatype systems: Firsov et al. build upon this de... View more
  • References (32)
    32 references, page 1 of 4

    Andreas Abel. 2010. MiniAgda: Integrating Sized and Dependent Types. Electronic Proceedings in Theoretical Computer Science 43 (Dec 2010), 14-28. https://doi.org/10.4204/eptcs.43.2

    Ki Yung Ahn. 2014. The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language based on Mendler-style Recursion Schemes and Term-indexed Types. (2014).

    Ki Yung Ahn and Tim Sheard. 2011. A Hierarchy of Mendler Style Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences. SIGPLAN Not. 46, 9 (Sept. 2011), 234-246. https://doi.org/10.1145/2034574.2034807

    Gilles Barthe, Maria Joao Frade, Eduardo Giménez, Luis Pinto, and Tarmo Uustalu. 2004. Type-based termination of recursive definitions. Mathematical structures in computer science 14, 1 (2004), 97-141.

    Frédéric Blanqui. 2005. Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae 65, 1-2 (2005), 61-86.

    Corrado Böhm. 1968. Alcune proprieta delle forme β -η-normali nel λ-K-calcolo. Pubblicazioni dell'Istituto per le Applicazioni del Calcolo 696 (1968), 19.

    Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552-593.

    R. M. Burstall, D. B. MacQueen, and D. T. Sannella. 1980. Hope: An Experimental Applicative Language.

    Thierry Coquand. 1992a. Pattern matching with dependent types. In Informal proceedings of Logical Frameworks, Vol. 92. 66-79.

    Thierry Coquand. 1992b. Pattern matching with dependent types. In Informal proceedings of Logical Frameworks, Vol. 92. 66-79.

  • Related Research Results (1)
  • Similar Research Results (2)
  • Metrics
Share - Bookmark