## 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

areas:

- Distributive systems and quantitative semantics (computer science). There

is a close relationship between these systems and semantics and differential

categories. - 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

**Location**:

Barrier lake Station, Kananakis Country, Alberta

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