Thesis icon

Thesis

The safe lambda calculus

Abstract:

We consider a syntactic restriction for higher-order grammars called safety that constrains occurrences of variables in the production rules according to their type-theoretic order. We transpose and generalize this restriction to the setting of the simply-typed lambda calculus, giving rise to what we call the safe lambda calculus. We analyze its expressivity and obtain a result in the same vein as Schwichtenberg's 1976 characterization of the simply-typed lambda calculus: the numeric functio...

Expand abstract

Actions


Access Document


Files:

Authors


More by this author
Institution:
University of Oxford
Research group:
Foundations, Logic and Structures
Oxford college:
Linacre College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
Role:
Author

Contributors

Role:
Supervisor
Publication date:
2009
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
URN:
uuid:537d45e0-01ac-4645-8aba-ce284ca02673
Local pid:
ora:2974

Terms of use


Metrics


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