Sökning: "Formalization of mathematics"

Visar resultat 1 - 5 av 6 avhandlingar innehållade orden Formalization of mathematics.

  1. 1. 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

  3. 2. Samspel mellan intuitiva idéer och formella bevis : en fallstudie av universitetsstudenters arbete med en analysuppgift

    Författare :Kerstin Pettersson; Högskolan i Skövde; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; MATHEMATICS; MATEMATIK; MATHEMATICS; MATEMATIK; MATHEMATICS; MATEMATIK;

    Sammanfattning : The aim of this study is to illuminate the interplay between intuitive ideas and formal justification. In a perspective where we focus on the students’ competences we describe the interaction between intuitive ideas and formal structures, as they appear especially in relation to concept definitions and formal proofs. LÄS MER

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

  5. 4. 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

  7. 5. Relations in Dependent Type Theory

    Författare :Carlos Gonzalía; Göteborgs universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; formalized mathematics; relational systems; category theory; programming logics; constructive type theory; logical frameworks; relational database model;

    Sammanfattning : This thesis investigates how to express and reason about relational concepts and methods inside the constructive logical framework of Martin-Löf's monomorphic type theory. We cover several areas where the notion of relation is central, and show how to formalize the basic concepts of each area. LÄS MER