# * On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer *

## by Robert L. Constable

2012

Invited talk at LICS 2012

**Abstract**

In this article I will examine a few key concepts and
design decisions that account for the high value of implemented
constructive type theories in computer science. Iâ€™ll stress the
historical fact that these theories, and the proof assistants that
animate them, were born from a strong partnership linking
computer science, logic, and mathematics.

I will recall how modern type theory researchers built on deep insights from the earliest pioneers: Turing â€“ the first computer scientist, Church â€“ the patriarch of logic in computer science, and Brouwer â€“ a singular pioneer of intuitionism and constructive mathematics. They created solid intellectual ground on which to build a formal implemented constructive theory of computation whose influence will be felt well beyond computing and information science alone. All generations of constructive type theory researchers since this beginning have had leaders from all three disciplines.

Much of the seminal modern work creating these type theories and their proof assistants was presented in LICS proceedings, and LICS could be a natural home for future work in this flourishing area which is the epitome of logic in computer science.

**bibTex ref: ConLICS12**

cite link