Sökning: "Anders Mörtberg"

Hittade 5 avhandlingar innehållade orden Anders Mörtberg.

  1. 1. Constructive Algebra in Type Theory

    Författare :Anders Mörtberg; Göteborgs universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : This thesis contains four papers aiming at bridging the gap between algorithms implemented in computer algebra systems and interactive proof assistants. This is done by implementing and verifying efficient algorithms using the Coq proof assistant together with the SSReflect extension. LÄS MER

  3. 2. Formalizing Refinements and Constructive Algebra in Type Theory

    Författare :Anders Mörtberg; Göteborgs universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formalization of mathematics; refinements; constructive algebra; type theory; Coq; SSReflect;

    Sammanfattning : The extensive use of computers in mathematics and engineering has led to an increased demand for reliability in the implementation of algorithms in computer algebra systems. One way to increase the reliability is to formally verify that the implementations satisfy the mathematical theorems stating their specification. LÄS MER

  4. 3. A Cubical Formalisation of Cohomology Theory and π4(S3) ≅ Z/2Z

    Författare :Axel Ljungström; Anders Mörtberg; Eric Finster; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Homotopy Type Theory; Cohomology; Formalisation;

    Sammanfattning : .... LÄS MER

  5. 4. Formalizing Univalent Set-Level Structures in Cubical Agda

    Författare :Max Zeuner; Anders Mörtberg; Martin Escardo; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : This licentiate thesis consists of two papers on formalization projects using Cubical Agda, a rather new extension of the Agda proof assistant with constructive support for univalence and higher inductive types. The common denominator of the two papers is that they are concerned with structures on types that are sets in the sense of Homotopy Type Theory or Univalent Foundations (HoTT/UF). LÄS MER

  7. 5. A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory

    Författare :Menno de Boer; Peter LeFanu Lumsdaine; Alexander Berglund; Bas Spitters; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Dependent type theory; Category theory; Contextual categories; Initiality; Formalization; Mathematics; matematik; matematisk logik; Mathematical Logic;

    Sammanfattning : In this licentiate thesis we present a proof of the initiality conjecture for Martin-Löf’s type theory with 0, 1, N, A+B, ∏AB, ∑AB, IdA(u,v), countable hierarchy of universes (Ui)iєN closed under these type constructors and with type of elements (ELi(a))iєN. We employ the categorical semantics of contextual categories. LÄS MER