東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Focusing on Modular Refinement Typing /

Economou, Dimitrios James,

Linked to FindBook

Google Book

Amazon

博客來

Focusing on Modular Refinement Typing /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Focusing on Modular Refinement Typing // Dimitrios James Economou.
Author:	Economou, Dimitrios James,
Description:	1 electronic resource (643 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 86-07, Section: B.
Contained By:	Dissertations Abstracts International86-07B.
Subject:	Design. -
Online resource:	https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31822514
ISBN:	9798302368744

Focusing on Modular Refinement Typing /
Economou, Dimitrios James,

Focusing on Modular Refinement Typing /Dimitrios James Economou. - 1 electronic resource (643 pages)

Source: Dissertations Abstracts International, Volume: 86-07, Section: B.

Refinement typing algorithms are hard to design and understand. Liquid Haskell (LH) has powerful features like modular, recursive refinement of inductive data. But Liquid Haskell is relatively hard to understand as it lacks an explicit phase distinction between indices and programs. Index based systems like Dependent ML (DML) tend toward less power but, enjoying an index-program phase distinction, are easier to understand. We apply techniques from logic, type theory, and category theory to design a correct and simple bidirectional typing algorithm for modular recursive index refinements. We use focusing to design logically a call-by-push-value (CBPV) with algebraic datatypes. CBPV is a language known empirically to have good semantic properties even in the presence of computational effects like nontermination and errors. Bidirectional type theories are a reliable way to combine rich type checking and inference. We prove our declarative system is semantically sound for standard mathematical models (domains). We prove our algorithmic system is decidable, sound, complete. Focusing and bidirectional typing combine elegantly with a new concept: value-determinedexistentials of input types under focus are guaranteed to be solved at the end of focusing stages, clearly outputting constraints decidable by an SMT solver. We believe this work improves our understanding of liquid refinement typing, and we hope it can guide or serve as the foundation for implementations thereof.

English

ISBN: 9798302368744Subjects--Topical Terms:

518875
Design.

Focusing on Modular Refinement Typing /
LDR:02674nmm a22003733i 4500 001 2436913
005 20251117053651.5
006 m o d
007 cr|nu||||||||
008 261011s2024 miu||||||m |||||||eng d
020 $a 9798302368744
035 $a (MiAaPQD)AAI31822514
035 $a AAI31822514
040 $a MiAaPQD $b eng $c MiAaPQD $e rda
100 1 $a Economou, Dimitrios James, $e author. $3 3827743
245 1 0 $a Focusing on Modular Refinement Typing / $c Dimitrios James Economou.
264 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2024
300 $a 1 electronic resource (643 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: Dissertations Abstracts International, Volume: 86-07, Section: B.
500 $a Advisors: Dunfield, Jana.
502 $b Ph.D. $c Queen's University (Canada) $d 2024.
520 $a Refinement typing algorithms are hard to design and understand. Liquid Haskell (LH) has powerful features like modular, recursive refinement of inductive data. But Liquid Haskell is relatively hard to understand as it lacks an explicit phase distinction between indices and programs. Index based systems like Dependent ML (DML) tend toward less power but, enjoying an index-program phase distinction, are easier to understand. We apply techniques from logic, type theory, and category theory to design a correct and simple bidirectional typing algorithm for modular recursive index refinements. We use focusing to design logically a call-by-push-value (CBPV) with algebraic datatypes. CBPV is a language known empirically to have good semantic properties even in the presence of computational effects like nontermination and errors. Bidirectional type theories are a reliable way to combine rich type checking and inference. We prove our declarative system is semantically sound for standard mathematical models (domains). We prove our algorithmic system is decidable, sound, complete. Focusing and bidirectional typing combine elegantly with a new concept: value-determinedexistentials of input types under focus are guaranteed to be solved at the end of focusing stages, clearly outputting constraints decidable by an SMT solver. We believe this work improves our understanding of liquid refinement typing, and we hope it can guide or serve as the foundation for implementations thereof.
546 $a English
590 $a School code: 0283
650 4 $a Design. $3 518875
650 4 $a Software. $2 gtt. $3 619355
650 4 $a Programming languages. $3 3683658
650 4 $a Algebra. $3 516203
650 4 $a Syntax. $3 897045
650 4 $a Logic. $3 529544
650 4 $a Semantics. $3 520060
650 4 $a Computer science. $3 523869
690 $a 0389
690 $a 0395
690 $a 0984
710 2 $a Queen's University (Canada). $e degree granting institution. $3 3765623
720 1 $a Dunfield, Jana $e degree supervisor.
773 0 $t Dissertations Abstracts International $g 86-07B.
790 $a 0283
791 $a Ph.D.
792 $a 2024
856 4 0 $u https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31822514