Reading Club

Description

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:

• Functional programming (e.g. Haskell)
• Generic programming
• Dependently-typed programming languages (e.g. Epigram, Agda)
• Proof assistants (e.g. Coq)
• Advanced type systems and extensions
• Category theory

Be sure to join our mailing list for up-to-date information.

Schedule

Visit the calendar or subscribe to the iCal version.

Topics

Current

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.

Proposed

These are articles that have been proposed for future meetings.

Longer reads

• Wouter Swierstra's PhD thesis (A Functional Specification of Effects)
• Edwin Brady's PhD thesis (Practical Implementation of a Dependently Typed Functional Programming Language)
• Johan Jeuring's PhD thesis (Theories for Algorithm Calculation)
• Doaitse Swierstra's PhD thesis (Lawine, an experiment in language and machine design)

Classical papers

• P. Landin. The Mechanical Evaluation of Expressions
• P. Landin. The next 700 programming languages

Miscellaneous

• Mark Jones. Language and Program Design for Functional Dependencies
• Neil Ghani and Patricia Johann. Initial Algebra Semantics is Enough!
• Last chapter of Alexey Rodriguez's PhD thesis
• Stefan Wehr and Manuel M. T. Chakravarty. ML Modules and Haskell Type Classes: A Constructive Comparison
• Pierce: Lenses
• Linguistics-oriented paper

Comics

From Piled Higher and Deeper: