We hold a weekly meeting to discuss the latest research, do challenging tutorials, or catch up on interesting theoretical background. Often, we're reading published articles from conferences and journals in the last few years. Topics that we find interesting include:
Be sure to join our mailing list
for up-to-date information.
Visit the calendar
or subscribe to the iCal version
These are articles that we have read in previous meetings or are planning to read in upcoming meetings. The list is organized with most recent (or planned) first.
- Programming in Martin-Löf's Type Theory - Bengt Nordstrom, Kent Petersson, Jan M. Smith, 1990.
- Definitional interpreters for higher-order programming languages - John C. Reynolds, 1972.
- Call-By-Push-Value: A Subsuming Paradigm - Paul Levy, Typed Lambda-Calculi and Applications, 1999.
- A substructural type system for backward strictness analysis - Stefan Holdermans and Jurriaan Hage, unpublished.
- Introduction to Categories in Computing - C. Barry Jay.
- Computational Category Theory - David Rydehaerd and Rod Burstall, 1988.
- Idioms are oblivious, arrows are meticulous, monads are promiscuous - A formal comparison between Moggi's monads, Hughes's arrows and McBride and Paterson's idioms.
- Scala for Generic Programmers - Datatype-generic programming in Scala.
- Category Theory for Program Construction by Calculation - Lambert Meertens. September, 1995. Lecture Notes for ESSLLI '95, Barcelona, Catalunya.
- Polytypic Programming in Coq - (WGP 2008) Formalization of type and term specialization of Generic Haskell-style programs in Coq.
- Ynot: Reasoning with the Awkward Squad - (ICFP 2008) An axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects.
- Foundations for Structured Programming with GADTs - (POPL'08) How the standard theory of datatypes as carriers of initial algebras of functors can be extended to encompass GADTs.
- Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures - (POPL'08) On how to encode Okasaki's algorithms analysis in dependent types.
- Clowns to the Left of me, Jokers to the Right - (POPL'08) Generalization of the derivative operation to the zipper.
- Trouble Shared is Trouble Halved - (Haskell'03) Sharing and memo functions.
- An idiom's guide to formlets - (Submitted to ICFP 2008) Formlets in Links decouple user interface from data, a vital form of abstraction supported by very few web frameworks. Formlets are best defined in terms of idioms, not monads or arrows as one might suppose from the existing literature.
- NixOS: A Purely Functional Linux Distribution - (Submitted to ICFP 2008) A purely functional system configuration model to avoid destructively updated system state.
- Typed Transformations of Typed Abstract Syntax - (Submitted to ICFP 2008) Supporting transformations of abstract syntax in a well-typed setting using GADTs, existential quantification, and lazy evaluation.
- Associated Type Synonyms - (ICFP 2005) Associated type synonyms constitute an interesting new alternative to explicit functional dependencies.
- Coq Tutorial - (POPL 2008) A tutorial on the use of the Coq proof assistant in formalizing programming language metatheory.
- Constructing Universes for Generic Programming - Peter Morris's PhD thesis on dependently typed programming in Epigram, strictly positive types/families, and containers.
These are articles that have been proposed for future meetings.
From Piled Higher and Deeper