Sökning: "agda"

Visar resultat 11 - 14 av 14 avhandlingar innehållade ordet agda.

1. 11. 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. 12. Verifying Information Flow Control Libraries

   Författare :Marco Vassena; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

   Sammanfattning : Information Flow Control (IFC) is a principled approach to protecting the confidentiality and integrity of data in software systems. Intuitively, IFC sys- tems associate data with security labels that track and restrict flows of information throughout a program in order to enforce security. LÄS MER

4. 13. 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. 14. 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