東華大學圖書館 |

語系: 繁體中文

說明(常見問題)

回圖書館首頁

手機版館藏查詢

登入

回首頁

切換: 標籤 | MARC模式 | ISBD

Relating justification logic modalit...

Pouliasis, Konstantinos.

FindBook

Google Book

Amazon

博客來

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

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Relating justification logic modality and type theory in Curry-Howard fashion./
作者:	Pouliasis, Konstantinos.
出版者:	Ann Arbor : ProQuest Dissertations & Theses, : 2018,
面頁冊數:	130 p.
附註:	Source: Dissertation Abstracts International, Volume: 79-05(E), Section: A.
Contained By:	Dissertation Abstracts International79-05A(E).
標題:	Logic. -
電子資源:	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