Sökning: "Martin-Löf type theory"

Visar resultat 1 - 5 av 10 avhandlingar innehållade orden Martin-Löf type theory.

1. 1. Reference and Computation in Intuitionistic Type Theory

   Författare :Johan G Granström; Erik Palmgren; Per Martin-Löf; Peter Dybjer; Uppsala universitet; []
   Nyckelord :mathematical logic; intuitionism; type theory; foundations of mathematics;

   Sammanfattning : Three topics, namely, computer science, philosophical logic, and mathematics, meet in intuitionistic type theory, which thus simultaneously is a programming language, a philosophy of language, and a foundation of mathematics. The present thesis compares, relates, and equates two concepts, one from philosophical logic and one from computer science, viz. LÄS MER

3. 2. A Natural Interpretation of Classical Proofs

   Författare :Jens Brage; Per Martin-Löf; Sara Negri; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Brouwer-Heyting-Kolmogorov; classical logic; constructive type theory; constructive semantics; proof interpretation; double-negation; continuation-passing-style; natural deduction; sequent calculus; cut elimination; explicit substitution; Mathematical logic; Matematisk logik;

   Sammanfattning : In this thesis we use the syntactic-semantic method of constructive type theory to give meaning to classical logic, in particular Gentzen's LK.We interpret a derivation of a classical sequent as a derivation of a contradiction from the assumptions that the antecedent formulas are true and that the succedent formulas are false, where the concepts of truth and falsity are taken to conform to the corresponding constructive concepts, using function types to encode falsity. LÄS MER

4. 3. Partiality and Choice : Foundational Contributions

   Författare :Jesper Carlström; Per Martin-Löf; Gilles Dowek; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; MATHEMATICS; MATEMATIK;

   Sammanfattning : The subject of the thesis is foundational aspects of partial functions (Papers 1, 2 & 4) and some choice principles (Papers 3 & 4) in the context of constructive mathematics.Paper 1 studies the inversion functions of commutative rings. The foundational problem of having them only partially defined is overcome by extending them to total functions. LÄS MER

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

7. 5. Cubical Intepretations of Type Theory

   Författare :Simon Huber; Göteborgs universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Dependent Type Theory; Univalence Axiom; Models of Type Theory; Identity Types; Cubical Sets;

   Sammanfattning : The interpretation of types in intensional Martin-Löf type theory as spaces and their equalities as paths leads to a surprising new view on the identity type: not only are higher-dimensional equalities explained as homotopies, this view also is compatible with Voevodsky's univalence axiom which explains equality for type-theoretic universes as homotopy equivalences, and formally allows to identify isomorphic structures, a principle often informally used despite its incompatibility with set theory. While this interpretation in homotopy theory as well as the univalence axiom can be justified using a model of type theory in Kan simplicial sets, this model can, however, not be used to explain univalence computationally due to its inherent use of classical logic. LÄS MER