Now showing items 1-2 of 2
Extensional concepts in intensional type theory
(University of Edinburgh. College of Science and Engineering. School of Informatics., 1995-07)
Theories of dependent types have been proposed as a foundation of constructive mathematics and as a framework in which to construct certified programs. In these applications an important role is played by identity types ...
Type Systems For Polynomial-time Computation
(Vom Fachbereich Mathematik der Technischen Universitat Darmstadt, 1999-02)
This thesis introduces and studies a typed lambda calculus with higher-order primitive recursion over inductive datatypes which has the property that all definable number-theoretic functions are polynomial time computable. ...