{"@context":"http://iiif.io/api/presentation/2/context.json","@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/manifest.json","@type":"sc:Manifest","label":"Mode-Sensitive Type Analysis for Prolog Programs","metadata":[{"label":"dc.description.sponsorship","value":"This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree."},{"label":"dc.format","value":"Monograph"},{"label":"dc.format.medium","value":"Electronic Resource"},{"label":"dc.identifier.uri","value":"http://hdl.handle.net/11401/77818"},{"label":"dc.language.iso","value":"en_US"},{"label":"dc.publisher","value":"The Graduate School, Stony Brook University: Stony Brook, NY."},{"label":"dcterms.abstract","value":"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  &quot; Well-typed programs can't go wrong&quot; . 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."},{"label":"dcterms.available","value":"2017-09-26T16:52:24Z"},{"label":"dcterms.contributor","value":"Warren, David S"},{"label":"dcterms.creator","value":"Hadjichristodoulou, Spyros"},{"label":"dcterms.dateAccepted","value":"2017-09-26T16:52:24Z"},{"label":"dcterms.dateSubmitted","value":"2017-09-26T16:52:24Z"},{"label":"dcterms.description","value":"Department of Computer Science."},{"label":"dcterms.extent","value":"161 pg."},{"label":"dcterms.format","value":"Monograph"},{"label":"dcterms.identifier","value":"Hadjichristodoulou_grad.sunysb_0771E_11863.pdf"},{"label":"dcterms.issued","value":"2014-05-01"},{"label":"dcterms.language","value":"en_US"},{"label":"dcterms.provenance","value":"Made available in DSpace on 2017-09-26T16:52:24Z (GMT). No. of bitstreams: 1\nHadjichristodoulou_grad.sunysb_0771E_11863.pdf: 752892 bytes, checksum: c988c363d560e9b996c3c2e36d06fc41 (MD5)\n  Previous issue date: 2014-05-01"},{"label":"dcterms.publisher","value":"The Graduate School, Stony Brook University: Stony Brook, NY."},{"label":"dcterms.subject","value":"Computer science"},{"label":"dcterms.title","value":"Mode-Sensitive Type Analysis for Prolog Programs"},{"label":"dcterms.type","value":"Dissertation"},{"label":"dc.type","value":"Dissertation"}],"description":"This manifest was generated dynamically","viewingDirection":"left-to-right","sequences":[{"@type":"sc:Sequence","canvases":[{"@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/canvas/page-1.json","@type":"sc:Canvas","label":"Page 1","height":1650,"width":1275,"images":[{"@type":"oa:Annotation","motivation":"sc:painting","resource":{"@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/47%2F88%2F72%2F47887215184900840549937304681605640787/full/full/0/default.jpg","@type":"dctypes:Image","format":"image/jpeg","height":1650,"width":1275,"service":{"@context":"http://iiif.io/api/image/2/context.json","@id":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/47%2F88%2F72%2F47887215184900840549937304681605640787","profile":"http://iiif.io/api/image/2/level2.json"}},"on":"https://repo.library.stonybrook.edu/cantaloupe/iiif/2/canvas/page-1.json"}]}]}]}