Sökning: "dependent types"

Visar resultat 1 - 5 av 1031 avhandlingar innehållade orden dependent types.

  1. 1. Univalent Types, Sets and Multisets : Investigations in dependent type theory

    Författare :Håkon Robbestad Gylterud; Erik Palmgren; Nicola Gambino; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; type theory; homotopy type theory; dependent types; constructive set theory; databases; formalisation; agda; Mathematics; matematik;

    Sammanfattning : This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. LÄS MER

  3. 2. 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

  4. 3. Functional Program Correctness Through Types

    Författare :Nils Anders Danielsson; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; well-typed syntax; normalisation by evaluation; program correctness; total languages; partial languages; lazy evaluation; time complexity; strong invariants; dependent types;

    Sammanfattning : This thesis addresses the problem of avoiding errors in functionalprograms. The thesis has three parts, discussing different aspects ofprogram correctness, with the unifying theme that types are anintegral part of the methods used to establish correctness. LÄS MER

  5. 4. Practical Unification for Dependent Type Checking

    Författare :Víctor López Juan; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; unification; type checking; dependent types; Functional Programming;

    Sammanfattning : When using popular dependently-typed languages such as Agda, Idris or Coq to write a proof or a program, some function arguments can be omitted, both to decrease code size and to improve readability.  Type checking such a program involves inferring a combination of these implicit arguments that makes the program type-correct. LÄS MER

  7. 5. Practical Heterogeneous Unification for Dependent Type Checking

    Författare :Víctor López Juan; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; unification; dependent types; type checking;

    Sammanfattning : Dependent types can specify in detail which inputs to a program are allowed, and how the properties of its output depend on the inputs. A program called the type checker assesses whether a program has a given type, thus detecting situations where the implementation of a program potentially differs from its intended behaviour. LÄS MER