國立虎尾科技大學 |

Relating justification logic modality and type theory in Curry-Howard fashion.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Relating justification logic modality and type theory in Curry-Howard fashion./
Author:	Pouliasis, Konstantinos.
Description:	1 online resource (130 pages)
Notes:	Source: Dissertation Abstracts International, Volume: 79-05(E), Section: A.
Contained By:	Dissertation Abstracts International79-05A(E).
Subject:	Logic. -
Online resource:	click for full text (PQDT)
ISBN:	9780355564242

Relating justification logic modality and type theory in Curry-Howard fashion.
Pouliasis, Konstantinos.

Relating justification logic modality and type theory in Curry-Howard fashion. - 1 online resource (130 pages)

Source: Dissertation Abstracts International, Volume: 79-05(E), Section: A.

Thesis (Ph.D.)--City University of New York, 2018.

Includes bibliographical references

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.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2018

Mode of access: World Wide Web

ISBN: 9780355564242Subjects--Topical Terms:

558909
Logic.
Index Terms--Genre/Form:

554714
Electronic books.

Relating justification logic modality and type theory in Curry-Howard fashion.
LDR:03320ntm a2200337Ki 4500 001 918052
005 20181022132814.5
006 m o u
007 cr mn||||a|a||
008 190606s2018 xx obm 000 0 eng d
020 $a 9780355564242
035 $a (MiAaPQ)AAI10685652
035 $a (MiAaPQ)minarees:14886
035 $a AAI10685652
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Pouliasis, Konstantinos. $3 1192279
245 1 0 $a Relating justification logic modality and type theory in Curry-Howard fashion.
264 0 $c 2018
300 $a 1 online resource (130 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertation Abstracts International, Volume: 79-05(E), Section: A.
500 $a Adviser: Sergei Artemov.
502 $a Thesis (Ph.D.)--City University of New York, 2018.
504 $a Includes bibliographical references
520 $a 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.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2018
538 $a Mode of access: World Wide Web
650 4 $a Logic. $3 558909
650 4 $a Theoretical mathematics. $3 1180455
655 7 $a Electronic books. $2 local $3 554714
690 $a 0395
690 $a 0642
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a City University of New York. $b Computer Science. $3 1184450
773 0 $t Dissertation Abstracts International $g 79-05A(E).
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10685652 $z click for full text (PQDT)