Abstracts.2018.DomainTheoryIntro

Introduction to Domain Theory with Agda

by Ayberk Tosun

Formulation of a denotational semantics for the untyped λ-calculus had eluded computer scientists for a while when a solution was given by Dana Scott [1] in 1969. This solution came through an insight into the algebraic essence of computability: that it can be interpreted as continuity. This in turn gave rise to domain theory, the study of domains which are the kind of structures suitable for giving semantics to general recursive languages. In my talk, I will give a brief introduction to domain theory and present an Agda formalization of it I have been working on.

References

[1] Scott, D. S. "A type-theoretical alternative to Cuch, Iswim, Owhy. Privately circulated memo." (1969): 411-440.