2019 Workshop on Foundational Methods in Computer Science

  • Start Date: 05/28/2019
  • End Date: 06/02/2019

Calgary, Alberta


Foundational Methods in Computer Science is an annual workshop that brings
togeher researchers in theoretical computer science and mathematics. Past
workshop have been held at Colgate University, Dalhousie University, Mount Allison
University, University of Ottawa, UBC, University of Washington (Spokane),
Reed College, and elsewhere. The meeting planned in Kananaskis in 2019 will
be the 27th meeting, and the 7th meeting hosted by the Barrier Lake Station
(also known as the Biogeoscience Institute) at the University of Calgary.


The relationship between computer science and mathematics stems directly
from the work of Haskell Curry in the 1930’s and W. A. Howard and Per MartinL¨of
in the 1960’s. In particular, the Curry-Howard correspondence establishes a
direct relationship between computer programs and mathematics proofs. Mathematically,
this relationship is best expressed using category theory, and can
be expressed more succictly as a direct correspondence between categories and
programming languages. Category theory, logic and computer scientists have
discussed their work and its implications to one another at FMCS meetings for
almost 30 years.


The themes of this year’s workshops will be differential and tangent categories,
higher category theory and applications of these. Our objective is to
facilitate a cross-pollination of ideas and concepts amongst computer scientists,
category theorists and other mathematicians with respect to our selected theme
and related topics. In particular, we will have four tutorials in the following



  • Distributive systems and quantitative semantics (computer science). There
    is a close relationship between these systems and semantics and differential
  • Tangent categories (category theory). These generalize the structure of
    classical differential geometry.
  • Functor calculus (homotopy theory). Goodwillie’s calculus establishes a
    kind of calculus for homotopy invariants like K-theory; abelian functor
    calculus is an example of a differential category.
  • Higher category theory (spans category theory and homotopy theory).
    This categorical structure is the basis for homotopy theory (mathematics)
    and homotopy type theory (computer science and logic).



Kristine Bauer, University of Calgary

Robin Cockett, University of Calgary

Other Information: 


Barrier lake Station, Kananakis Country, Alberta


More details on the program and registration will be made available soon.