| dc.identifier.uri | http://hdl.handle.net/11401/77818 | |
| dc.description.sponsorship | This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree. | en_US |
| dc.format | Monograph | |
| dc.format.medium | Electronic Resource | en_US |
| dc.language.iso | en_US | |
| dc.publisher | The Graduate School, Stony Brook University: Stony Brook, NY. | |
| dc.type | Dissertation | |
| dcterms.abstract | Type systems are popular tools programmers use to write bug-free programs easily. In many cases, type systems also offer the benefit of theoretical guarantees with respect to the program's behavior; such statements are usually phrased in type-system slang as " Well-typed programs can't go wrong" . In the context of Prolog, two different treatments of types have been employed in various type systems. <italic>Descriptive</italic> (or regular) types, which are over-approximations of the success set of a program, characterize programs as well-typed based on the program's contents, in a way that everything true in the program is also well-typed. A common application of type systems with descriptive types is in <italic>termination analysis</italic>. On the other hand, <italic>prescriptive</italic> types are used to best describe legitimate ways of calling Prolog predicates, hence provide a better discrimination on well-typedness versus success/failure in Prolog. Prescriptively typed systems are most commonly used for helping users in debugging their programs. In this thesis we present the design and operational semantics of a new type system with parametric and subtyping polymorphism for Prolog in the context of prescriptive types, called P<subscript><:</subscript>. What distinguishes P<subscript><:</subscript> from other type systems proposed for Prolog, is that <italic>mode information</italica> is used along with the types of the predicates' arguments for ensuring well-typedness. In its initial design, P<subscript><:</subscript> uses <italic>zero-context</italic> mode information, and is extended to use <italic>type-mode</italic> information from any custom inferencer later on. We use <italic>Bounded Quantification</italic> in the form of <italic>Universal</italic> and <italic>Existential</italic> types to define a richer language of expressing type signatures. We also introduce the notion of <italic>annotations</italic> to type variables as a natural way to represent typings in P<subscript><:</subscript> , which allows us to express (sub)type checking using standard unification, and appropriate definitions for <italic>replacements</italic> and <italic>substitutions</italic>. Furthermore, we provide a well-typedness argument specifically tailored for Prolog programs, guaranteeing that for a given well-typed program-query pair, all answers inferred will be well-typed. Finally, we make P<subscript><:</subscript> easily used in practice with an inference algorithm for the types of program variables, in order to ensure well-typedness with minimal annotations in the program. | |
| dcterms.available | 2017-09-26T16:52:24Z | |
| dcterms.contributor | Warren, David | en_US |
| dcterms.contributor | Warren, David S | en_US |
| dcterms.contributor | Kifer, Michael | en_US |
| dcterms.contributor | Liu, Yanhong | en_US |
| dcterms.contributor | Ramakrishnan, C.R. | en_US |
| dcterms.contributor | Papaspyrou, Nikolaos. | en_US |
| dcterms.creator | Hadjichristodoulou, Spyros | |
| dcterms.dateAccepted | 2017-09-26T16:52:24Z | |
| dcterms.dateSubmitted | 2017-09-26T16:52:24Z | |
| dcterms.description | Department of Computer Science. | en_US |
| dcterms.extent | 161 pg. | en_US |
| dcterms.format | Monograph | |
| dcterms.format | Application/PDF | en_US |
| dcterms.identifier | Hadjichristodoulou_grad.sunysb_0771E_11863.pdf | en_US |
| dcterms.identifier | http://hdl.handle.net/11401/77818 | |
| dcterms.issued | 2014-05-01 | |
| dcterms.language | en_US | |
| dcterms.provenance | Submitted by Jason Torre (fjason.torre@stonybrook.edu) on 2017-09-26T16:52:24Z
No. of bitstreams: 1
Hadjichristodoulou_grad.sunysb_0771E_11863.pdf: 752892 bytes, checksum: c988c363d560e9b996c3c2e36d06fc41 (MD5) | en |
| dcterms.provenance | Made available in DSpace on 2017-09-26T16:52:24Z (GMT). No. of bitstreams: 1
Hadjichristodoulou_grad.sunysb_0771E_11863.pdf: 752892 bytes, checksum: c988c363d560e9b996c3c2e36d06fc41 (MD5)
Previous issue date: 2014-05-01 | en |
| dcterms.publisher | The Graduate School, Stony Brook University: Stony Brook, NY. | |
| dcterms.subject | Formal Methods, Logic Programming, Programming Languages, Type Systems | |
| dcterms.subject | Computer science | |
| dcterms.title | Mode-Sensitive Type Analysis for Prolog Programs | |
| dcterms.type | Dissertation | |
