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
Oxford college:
Merton College
Department:
Mathematical,Physical & Life Sciences Division - Computer Science,Department of

Contributors

Role:
Supervisor
Publication date:
2014
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
URN:
uuid:46b7bc70-3dfe-476e-92e7-245b7629ae4e
Local pid:
ora:8286

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP