Sökning: "inductive types"

Visar resultat 1 - 5 av 43 avhandlingar innehållade orden inductive types.

1. 1. On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory

   Författare :Andrea Vezzosi; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Conversion; Parametricity; Higher Inductive Types; Sized Types; Dependent Types; Type Theory; Guarded Types;

   Sammanfattning : Martin Löf Type Theory, having put computation at the center of logical reasoning, has been shown to be an effective foundation for proof assistants, with applications both in computer science and constructive mathematics. One ambition though is for MLTT to also double as a practical general purpose programming language. LÄS MER

3. 2. Tree Transformations in Inductive Dependency Parsing

   Författare :Jens Nilsson; Joakim Nivre; Pierre Nugues; Växjö universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Inductive Dependency Parsing; Dependency Structure; Tree Transformation; Non-projectivity; Coordination; Verb Group; Language technology; Språkteknologi; Computer and Information Sciences Computer Science; Data- och informationsvetenskap;

   Sammanfattning : This licentiate thesis deals with automatic syntactic analysis, or parsing, of natural languages. A parser constructs the syntactic analysis, which it learns by looking at correctly analyzed sentences, known as training data. The general topic concerns manipulations of the training data in order to improve the parsing accuracy. LÄS MER

4. 3. Tree Transformations in Inductive Dependency Parsing

   Författare :Jens Nilsson; Joakim Nivre; Pierre Nugues; Växjö universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Inductive Dependency Parsing; Dependency Structure; Tree Transformation; Non-projectivity; Coordination; Verb Group; Language technology; Språkteknologi; Computer and Information Sciences Computer Science; Data- och informationsvetenskap;

   Sammanfattning : This licentiate thesis deals with automatic syntactic analysis, or parsing, of natural languages. A parser constructs the syntactic analysis, which it learns by looking at correctly analyzed sentences, known as training data. The general topic concerns manipulations of the training data in order to improve the parsing accuracy. LÄS MER

5. 4. Exact completion and type-theoretic structures

   Författare :Jacopo Emmenegger; Erik Palmgren; Alexander Berglund; Maria Emilia Maietti; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; exact completion; type theory; setoid; weak limits; cartesian closure; inductive types; Mathematics; matematik;

   Sammanfattning : This thesis consists of four papers and is a contribution to the study of representations of extensional properties in intensional type theories using, mainly, the language and tools from category theory. Our main focus is on exact completions of categories with weak finite limits as a category-theoretic description of the setoid construction in Martin-Löf's intensional type theory. LÄS MER

7. 5. Precise Reasoning About Non-strict Functional Programs; How to Chase Bottoms, and How to Ignore Them

   Författare :Nils Anders Danielsson; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; partial; inductive; coinductive; non-strict; equational reasoning; lifted; infinite; functional programming;

   Sammanfattning : This thesis consists of two parts. Both concern reasoning about non-strict functional programming languages with partial and infinite values and lifted types, including lifted function spaces.The first part is a case study in program verification: We have written a simple parser and a corresponding pretty-printer in Haskell. LÄS MER