#### 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