Escardó, Martin
Tutorials
Theory and Practice of Highertype Computation (Tutorial)
Abstract
In highertype computation, established by Kleene and Kreisel in the late 1950's (independently), one works with the data types obtained from the discrete natural numbers by closing under finite products and function spaces. For the theory of highertype programming languages, it is natural to work with a corresponding hierarchy, or type structure, of domains, identified by Ershov and Scott in the late 1960's (again independently). The KleeneKreisel and ErshovScott hierarchies account for total and partial computation respectively.
In this tutorial I'll explain the theory and practice of highertype computation and programming languages, and develop old and new applications.
From a theoretical point of view, I'll present KleeneKreisel spaces and ErshovScott domains, and relate the two. Moreover, I'll discuss common generalizations, chiefly QCB spaces and equilogical spaces, which admit further useful closure properties, and their relationship to TTE (Schroeder, Simpson. Scott, Bauer, Weihrauch and many others). I'll also present a natural highertype model of computation/programming language, namely PCF (Platek, Scott, Plotkin).
From a practical point of view, I'll introduce a fragment of the language Haskell as a faithful implementation of PCF. Moreover, I'll develop and run several examples (and prove theorems about them), pertaining to (i) exhaustive search of infinite sets in finite time in particular Ulrich Berger's algorithm and generalizations), and (ii) computation with real numbers (in particular Alex Simpson's integration algorithm and generalizations).
BibTeX  Entry
@InProceedings{escard:OASIcs:2009:2254,
author = {Martin Escard{\'o}},
title = {{Theory and Practice of Highertype Computation (Tutorial)}},
booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {9783939897125},
ISSN = {21906807},
year = {2009},
volume = {11},
editor = {Andrej Bauer and Peter Hertling and KerI Ko},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2009/2254},
URN = {urn:nbn:de:0030drops22540},
doi = {http://dx.doi.org/10.4230/OASIcs.CCA.2009.2254},
annote = {Keywords: Highertype computation, domain theory, KleeneKreisel spaces, ErshovScott domains, QCB spaces, equilogical spaces, PCF}
}
2009
Keywords: 

Highertype computation, domain theory, KleeneKreisel spaces, ErshovScott domains, QCB spaces, equilogical spaces, PCF 
Seminar: 

6th International Conference on Computability and Complexity in Analysis (CCA'09)

Related Scholarly Article: 


Issue date: 

2009 
Date of publication: 

2009 