東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Relating justification logic modalit...

Pouliasis, Konstantinos.

Linked to FindBook

Google Book

Amazon

博客來

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

Record Type:	Electronic resources : Monograph/item
Title/Author:	Relating justification logic modality and type theory in Curry-Howard fashion./
Author:	Pouliasis, Konstantinos.
Published:	Ann Arbor : ProQuest Dissertations & Theses, : 2018,
Description:	130 p.
Notes:	Source: Dissertation Abstracts International, Volume: 79-05(E), Section: A.
Contained By:	Dissertation Abstracts International79-05A(E).
Subject:	Logic. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10685652
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. - Ann Arbor : ProQuest Dissertations & Theses, 2018 - 130 p.

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

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

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.

ISBN: 9780355564242Subjects--Topical Terms:

529544
Logic.

Relating justification logic modality and type theory in Curry-Howard fashion.
LDR:03037nmm a2200301 4500 001 2163535
005 20181022132814.5
008 190424s2018 ||||||||||||||||| ||eng d
020 $a 9780355564242
035 $a (MiAaPQ)AAI10685652
035 $a (MiAaPQ)minarees:14886
035 $a AAI10685652
040 $a MiAaPQ $c MiAaPQ
100 1 $a Pouliasis, Konstantinos. $3 3351557
245 1 0 $a Relating justification logic modality and type theory in Curry-Howard fashion.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2018
300 $a 130 p.
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.
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.
590 $a School code: 0046.
650 4 $a Logic. $3 529544
650 4 $a Theoretical mathematics. $3 3173530
690 $a 0395
690 $a 0642
710 2 $a City University of New York. $b Computer Science. $3 1029886
773 0 $t Dissertation Abstracts International $g 79-05A(E).
790 $a 0046
791 $a Ph.D.
792 $a 2018
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10685652