Sökning: "types"

Visar resultat 1 - 5 av 7851 avhandlingar innehållade ordet types.

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

    Författare :Andrea Vezzosi; Chalmers University of Technology; []
    Nyckelord :NATURVETENSKAP; NATURVETENSKAP; NATURAL SCIENCES; 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

  2. 2. Guarded Recursive Types in Type Theory

    Författare :Andrea Vezzosi; Chalmers University of Technology; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; sized types; induction; coinduction; type theory; totality; guarded types; Agda;

    Sammanfattning : In total functional (co)programming valid programs are guaranteed to always produce (part of) their output in a finite number of steps.Enforcing this property while not sacrificing expressivity has beenchallenging. LÄS MER

  3. 3. Types for XML with Application to Xcerpt

    Författare :Artur Wilk; Wlodzimierz Drabent; Jan Maluszýnski; Franciois Bry; Linköpings universitet; []
    Nyckelord :NATURAL SCIENCES; NATURVETENSKAP; NATURVETENSKAP; NATURAL SCIENCES; XML; types; Xcerpt; XML schema; ontologies; XML querying; Computer science; Datavetenskap;

    Sammanfattning : XML data is often accompanied by type information, usually expressed by some schema language. Sometimes XML data can be related to ontologies defining classes of objects, such classes can also be interpreted as types. Type systems proved to be extremely useful in programming languages, for instance to automatically discover certain kinds of errors. LÄS MER

  4. 4. Functional Program Correctness Through Types

    Författare :Nils Anders Danielsson; Chalmers University of Technology; []
    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. 5. Univalent Types, Sets and Multisets : Investigations in dependent type theory

    Författare :Håkon Robbestad Gylterud; Erik Palmgren; Nicola Gambino; Stockholms universitet; []
    Nyckelord :NATURAL SCIENCES; NATURVETENSKAP; 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