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
Division:
MPLS
Department:
Computer Science
Research group:
Foundations, Logic and Structures
Oxford college:
Linacre College
Role:
Author

Contributors

Division:
MPLS
Department:
Computer Science
Role:
Supervisor
Publication date:
2009
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
Language:
English
Keywords:
Subjects:
UUID:
uuid:537d45e0-01ac-4645-8aba-ce284ca02673
Local pid:
ora:2974
Deposit date:
2009-10-05

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