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).
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.
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
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).
Categorial and Categorical Grammars
Tuesday 2011-05-17: EDIT room
Categorical Semantics for Arrows
Categorical De Morgan laws
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
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.
A Core Calculus of Dependency
12.10. Lunch & Closing.
Register here for a presentation of a paper/book chapter by writing your name and a reference to the document.
- (Retracted) When is a Refinement Type an Inductive Type
- Factorizing folds
- Internal Diagrams in Category Theory
- The Expression Lemma
- Fibrational Induction Rules for Initial Algebras*
- Modified realizability toposes and strong normalization proofs
- Categorial and Categorical Grammars
- Category Theoretical Semantics for Pregroup Grammars
- A Compositional Distributional Model of Meaning
- A Core Calculus of Dependency, Abadi et.al.
- A Categorical Unification Algorithm, Rydeheard and Burstall
- preliminary Categorical De Morgan laws
- Elementary Categories, Elementary Toposes, C. McLarty; first chapters of Part 3 "Toposes"
- An informal introduction to topos theory
- Sheaves in Geometry and Logic, S. MacLane and I. Moerdijk