Sökning: "Per Martin-Löf"
Hittade 5 avhandlingar innehållade orden Per Martin-Löf.
1. Notes on constructive mathematics
Sammanfattning : .... LÄS MER
2. A Natural Interpretation of Classical Proofs
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
3. Partiality and Choice : Foundational Contributions
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
4. Reference and Computation in Intuitionistic Type Theory
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
5. A Type Theoretical Analysis of Some Aspects of Programming Languages
Sammanfattning : We present three papers on the application of Martin-Löf's type theory to the analysis of programming languages. In the first paper, we present formal proofs in type theory of the combinatorial completeness of two calculi of combinators. The statement formulates the ability of the calculi to describe functions. LÄS MER