Avancerad sökning

Visar resultat 1 - 5 av 102 avhandlingar som matchar ovanstående sökkriterier.

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

  5. 4. Learning to learn in e-Learning : constructive practices for development

    Författare :Annika Andersson; Åke Grönlund; Karin Hedström; Tim Unwin; Örebro universitet; []
    Nyckelord :SAMHÄLLSVETENSKAP; SOCIAL SCIENCES; ICT4D; distance education; constructive learning practices; Structuration Theory; ICT; developing countries; e-learning; Informatics; Informatik; Informatik; Informatics;

    Sammanfattning : This thesis concerns technology use in distance educations and learning practices related to this use. The research was carried out over the period 2005 to 2009 in Bangladesh and Sri Lanka and has been reported in 6 published papers. LÄS MER

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