Thesis icon

Thesis

Analysis and synthesis of inductive families

Abstract:

Based on a natural unification of logic and computation, Martin-Löf’s intuitionistic type theory can be regarded simultaneously as a computationally meaningful higher-order logic system and an expressively typed functional programming language, in which proofs and programs are treated as the same entities. Two modes of programming can then be distinguished: in externalism, we construct a program separately from its correctness proof with respect to a given specification, ...

Expand abstract

Actions


Access Document


Files:

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
University College
Role:
Author

Contributors

Division:
MPLS
Department:
Computer Science
Role:
Supervisor
Publication date:
2014
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
Language:
English
Keywords:
UUID:
uuid:2bc39bde-ce59-4a49-b499-3afdf174bbab
Local pid:
ora:9019
Deposit date:
2014-10-06

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP