Dissertations, Theses, and Capstone Projects
Date of Degree
2-2018
Document Type
Dissertation
Degree Name
Ph.D.
Program
Computer Science
Advisor
Sergei Artemov
Committee Members
Melvin Fitting
Subash Shankar
Stathis Zachos
Subject Categories
Other Computer Sciences | Programming Languages and Compilers | Theory and Algorithms
Keywords
type theory, justification logic, modal logic, functional programming, Curry--Howard isomorphism
Abstract
This dissertation is a work in the intersection of Justification Logic and Curry--Howard Isomorphism. Justification logic is an umbrella of modal logics of knowledge with explicit evidence. Justification logics have been used to tackle traditional problems in proof theory (in relation to Godel's provability) and philosophy (Gettier examples, Russel's barn paradox). The Curry--Howard Isomorphism or proofs-as-programs is an understanding of logic that places logical studies in conjunction with type theory and -- in current developments -- category theory. The point being that understanding a system as a logic, a typed calculus and, a language of a class of categories constitutes a useful discovery that can have many applications. The applications we will be mainly concerned with are type systems for useful programming language constructs. This work is structured in three parts: The first part is a a bird's eye view into my research topics: intuitionistic logic, justified modality and type theory. The relevant systems are introduced syntactically together with main metatheoretic proof techniques which will be useful in the rest of the thesis. The second part features my main contributions. I will propose a modal type system that extends simple type theory (or, isomorphically, intuitionistic propositional logic) with elements of justification logic and will argue about its computational significance. More specifically, I will show that the obtained calculus characterizes certain computational phenomena related to linking (e.g. module mechanisms, foreign function interfaces) that abound in semantics of modern programming languages. I will present full metatheoretic results obtained for this logic/ calculus utilizing techniques from the first part and will provide proofs in the Appendix. The Appendix contains also information about an implementation of our calculus in the metaprogramming framework Makam. Finally, I conclude this work with a small ``outro'', where I informally show that the ideas underlying my contributions can be extended in interesting ways.
Recommended Citation
Pouliasis, Konstantinos, "Relating Justification Logic Modality and Type Theory in Curry–Howard Fashion" (2018). CUNY Academic Works.
https://academicworks.cuny.edu/gc_etds/2455
Included in
Other Computer Sciences Commons, Programming Languages and Compilers Commons, Theory and Algorithms Commons