Date | Speaker | Title | Extra |
---|---|---|---|
Dec 12 | Ulf Norell | Structurally recursive descent parsing | abstract |
Dec 5 | Martin Hofmann | Difunctional Relations and their application to effect-based program transformation | abstract |
Dec 4 | Anton Setzer | Inductive-recursive definitions and partial recursive functions | abstract |
Nov 21 | Nils Anders Danielsson | A Formalisation of the Correctness Result From "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures" | abstract |
Nov 14 | Lars Birkedal | A Realizability Model of Hoare Type Theory | abstract, slides |
Oct 17 | Randy Pollack | Locally nameless representation and nominal Isabelle | abstract |
Oct 10 | Thierry Coquand and Peter Dybjer | |
abstract |
Oct 3 | Patrik Jansson | Highlights from IFIP 2.1 meeting | abstract |
Sep 26 | Carsten Schürmann | A gentle introduction to Delphin | abstract |
Sep 19 | Fredrik Lindblad | Automated Proof Construction based on Narrowing | abstract |
Sep 14 | Neil D. Jones | The Semantics of ``Semantic Patches" in Coccinelle | abstract, mailto:neil@diku.dk |
Sep 13 | Ralph Matthes | Verification of programs involving nested datatypes in intensional type theory | abstract |
Aug 28 | Venanzio Capretta | Common Knowledge as a Coinductive Modality | abstract |
Jun 27 | Nils Anders Danielsson | Internal automation and metaprogramming | abstract |
Jun 20 | Alexandre Buisse | Formalizing categorical models of type theory inside type theory | abstract |
Jun 6 | |
nationaldagen | |
May 30 | |
AIM6 | |
May 23 | Mats Jansborg | Translating Haskell into Agda | abstract |
May 16 | Ulf Norell | The with-construct: pattern matching on intermediate results | abstract |
May 9 | |
AIM6 planning | |
May 2 | |
TYPES | |
Apr 18 | Nils Anders Danielsson | Verification of a Simple Library for Semi-Formal Verification of the Time Complexity of Purely Functional Data Structures | abstract |
Apr 4 | Peter Dybjer | Recent news on normalization by evaluation for type theory | abstract, slides |
Mar 28 | |
VR-applications | |
Mar 21 | Arnaud Spiwack | Towards Homological Algebra in Type Theory - A Glimpse in Dependent Type Programming | abstract |
Mar 14 | Andreas Abel | Some syntactical normalization proofs | abstract |
Mar 7 | Thierry Coquand | What is a model of type theory? | abstract, slides |
Feb 28 | Makoto Takeyama | Agda Core Checker Implementation, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-building | abstract |
Feb 7 | Randy Pollack | Some Recent Logical Frameworks | slides |
Jan 31 | Nils Anders Danielsson | A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family | abstract |
Jan 24 | Ulf Norell | A Module System for Agda, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-building | abstract, slides |