Thesis icon

Thesis

In search of effectful dependent types

Abstract:

Real world programming languages crucially depend on the availability of computational effects to achieve programming convenience and expressive power as well as program efficiency. Logical frameworks rely on predicates, or dependent types, to express detailed logical properties about entities. According to the Curry-Howard correspondence, programming languages and logical frameworks should be very closely related. However, a language that has both good support for real programming and ser...

Expand abstract

Actions


Access Document


Files:

Authors


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

Contributors

Role:
Supervisor
More from this funder
Funding agency for:
Vákár, M
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
University of Oxford
UUID:
uuid:e91e19b3-7e10-4fda-9433-f23b469e4049
Deposit date:
2017-12-14

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