Recent Changes - Search:
CTFP11 /

Presentations

Abstracts and schedule for the final presentations of the CTFP course 2011

Thursday 2011-05-12: EDIT-room

10.00. Guilhem (slides)

For any inductive datatype (ie, that is the carrier of the initial F-algebra), Lambek's Lemma provides an iteration operator fold that can eg, be used to derive an induction rule for the type if the functor F is polynomial. I'll show how to bypass this restriction and find an inductive schema to prove that some notion of property holds for the inhabitants of any inductive type (without any condition on the functor F).

10.35. Jean-Philippe:

I will review the initial algebra interpretation of data, then explain the notion of catamorphism, as well as the "fusion/fisson" rule. Then I will show how this rule can be used to optimise certain functional programs on a couple of examples.

11.10. Anders:

I will present a framework of adjunctions and functors that can be used to rewrite many programs as folds and unfolds to make them suitable for optimization, e.g fusion. I will give examples showing how to apply the framework to currying and mutual value recursion.

11.45 Lunch break

13.00. Tobias

I will showcase an approach, relying on the Yoneda Lemma and adjunctions, to establish isomorphisms between types that focuses on showing existence rather then deriving witnesses. At the beginning of the talk I will show how to establish some very simple isomorphism (inspired by "high-school algebra" laws) using this approach. Then I will in briefly review the concept of fixpoints and present the "rolling rules" and the "diagonal rules". At the end I will show how we can use all of our new knowledge to establish the isomorphisms between recursive types. For example: BinaryTree ≅ List ∘ Rose and Rose ≅ Fork (rose trees and fork trees).

13.35. Ramona

Categorial and Categorical Grammars

14.10. Close.

Tuesday 2011-05-17: EDIT room

9.00. Willard

Categorical Semantics for Arrows

9.35. Ann

Categorical De Morgan laws

10.10. Dan:

I will talk about some building primitives in dependently typed languages (Pi-types, Sigma-types, etc), show how typing rules for these types are established and how this connects with category theory: what context morphisms are, and how one can get a model of a given type theory using categories with families.

Around 10.45: Coffee break

11.00. Simon

Each topos gives rise to an internal language which is sound for topos logic, an intuitionistic higher-order logic. This allows reasoning about objects and morphisms of a topos in a more set-theoretical language. After a short recap of the notion of a topos, I will introduce the internal language and topos logic; then I will give some examples of theorems which hold in topos logic.

11.35. Arnar

A Core Calculus of Dependency

12.10. Lunch & Closing.

Registrations

Register here for a presentation of a paper/book chapter by writing your name and a reference to the document.

Jean-Philippe
Willard
Categorical Semantics for Arrows (direct link; access from within Chalmers network)
Guilhem
Ramona
Dan
Anders
Tobias
Arnar
Ann
Simon