Sponsor
Portland State University. Department of Computer Science
First Advisor
Tim Sheard
Date of Publication
Fall 12-16-2014
Document Type
Dissertation
Degree Name
Doctor of Philosophy (Ph.D.) in Computer Science
Department
Computer Science
Subjects
Programming languages (Electronic computers), Lambda calculus, Curry-Howard isomorphism
DOI
10.15760/etd.2086
Physical Description
1 online resource (xiii, 347 pages)
Abstract
Two major applications of lambda calculi in computer science are functional programming languages and mechanized reasoning systems (or, proof assistants). According to the Curry--Howard correspondence, it is possible, in principle, to design a unified language based on a typed lambda calculus for both logical reasoning and programming. However, the different requirements of programming languages and reasoning systems make it difficult to design such a unified language that provides both. Programming languages usually extend lambda calculi with programming-friendly features (e.g., recursive datatypes, general recursion) for supporting the flexibility to model various computations, while sacrificing logical consistency. Logical reasoning systems usually extend lambda calculi with logic-friendly features (e.g., induction principles, dependent types) for paradox-free inference over fine-grained properties, while being more restrictive in modeling computations.
In this dissertation, we design and implement a language called Nax that embraces benefits of both. Nax accepts all recursive datatypes, thus, allowing the same flexibility of defining recursive datatypes as in functional languages. Nax supports a number of Mendler-style recursion schemes that can express various kinds of recursive computations and also guarantee termination. Nax supports term-indexed types to support specifications of fine-grained properties. In addition, Nax supports a conservative extension of Hindley--Milner type inference.
The theoretical contributions of this dissertation include theories for Mendler-style recursion schemes and term-indexed types, which we developed to establish strong normalization and logical consistency of Nax.
Persistent Identifier
http://archives.pdx.edu/ds/psu/13198
Recommended Citation
Ahn, Ki Yung, "The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language based on Mendler-style Recursion Schemes and Term-indexed Types" (2014). Dissertations and Theses. Paper 2088.
https://pdxscholar.library.pdx.edu/open_access_etds/2088
10.15760/etd.2086