This site contains wikipages for the department of computer science and engineering at Chalmers and GU. 
CTFP11 /
PresentationsAbstracts and schedule for the final presentations of the CTFP course 2011Thursday 20110512: EDITroom10.00. Guilhem (slides)For any inductive datatype (ie, that is the carrier of the initial Falgebra), 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. JeanPhilippe: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 break13.00. TobiasI 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 "highschool 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. RamonaCategorial and Categorical Grammars 14.10. Close.Tuesday 20110517: EDIT room9.00. WillardCategorical Semantics for Arrows 9.35. AnnCategorical De Morgan laws 10.10. Dan:I will talk about some building primitives in dependently typed languages (Pitypes, Sigmatypes, 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 break11.00. SimonEach topos gives rise to an internal language which is sound for topos logic, an intuitionistic higherorder logic. This allows reasoning about objects and morphisms of a topos in a more settheoretical 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. ArnarA Core Calculus of Dependency 12.10. Lunch & Closing.RegistrationsRegister here for a presentation of a paper/book chapter by writing your name and a reference to the document.
