Thesis icon

Thesis

Intersection types and higer-order model checking

Abstract:

Higher-order recursion schemes are systems of equations that are used to define finite and infinite labelled trees. Since, as Ong has shown, the trees defined have a decidable monadic second order theory, recursion schemes have drawn the attention of research in program verification, where they sit naturally as a higher-order, functional analogue of Boolean programs. Driven by applications, fragments have been studied, algorithms developed and extensions proposed; the emerging theme is c...

Expand abstract

Actions


Access Document


Files:

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Merton College
Role:
Author
More by this author
Division:
MPLS
Department:
Computer Science
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:
Subjects:
UUID:
uuid:46b7bc70-3dfe-476e-92e7-245b7629ae4e
Local pid:
ora:8286
Deposit date:
2014-04-10

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