index.html

### default.html(section.main=current)

<h2>Research Themes</h2>

<p>
  Our vision is to use <strong>mathematics to understand the nature of
  computation</strong>, and to turn that understanding into
  the <strong>next generation of programming languages</strong>.

<p>
  We see the mathematical foundations of computation and programming as
  inextricably linked. We study one so as to develop the other.

<p>
  This reflects the symbiotic relationship between mathematics,
  programming, and the design of programming languages &mdash; any attempt to
  sever this connection will diminish each component.

<p>
  To achieve these research goals we use ideas from the following
  disciplines:

<dl>
  <dt>Functional Programming</dt>
  <dd>
    What does the future of programming languages look like?
    Functional programming languages
    like <a href="http://www.haskell.org/">Haskell</a>, <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda
    2</a> and Epigram are currently at the apex of programming
    language design and so form our target model of computation.
  </dd>

  <dt>Logic</dt>
  <dd>
    Why is functional programming successful as a model of
    computation? The answer lies in its genesis as a clean
    implementation of the logical structure of computation. Thus we
    develop functional programming by studying the logical structure
    of computation.
  </dd>

  <dt>Type Theory</dt>
  <dd>
    How does one take the logical structure of computation and turn it
    into a programming abstraction? Type theory allows us to do this
    by providing a language at an intermediate level of abstraction
    between a programming language and its logical
    foundations. Indeed, type theory could be said to be the ideas
    factory for programming languages.
  </dd>

  <dt>Category Theory</dt>
  <dd>
    How does one understand structure abstractly?  One uses category
    theory—that's how! Ideas such as monads and initial algebra
    semantics attest to the deep contribution that category theory has
    made to computation.
  </dd>
</dl>