2009
October 20, 2009 - Programming with proofs and explicit contexts
October 13, 2009 - Formal verification of a realistic compiler
October 6, 2009 - Beautiful differentiation
September 29, 2009 - Verifying correct usage of atomic blocks and typestate
September 15, 2009 - The Proof Theory and Semantics of Intuitionistic Modal Logic
September 15, 2009 - Modal Types for Mobile Code
September 8, 2009 - A judgmental reconstruction of modal logic
September 1, 2009 - Space profiling for parallel functional programs
August 25, 2009 - Proofs and types
August 18, 2009 - The Semantics of Predicate Logic as a Programming Language
August 18, 2009 - The "simplest functional programming language" is neither simple nor functional
August 18, 2009 - Implementation and applications of Scott's logic for computable functions
August 11, 2009 - A predicative analysis of structural recursion
July 28, 2009 - Design of the programming language FORSYTHE
July 14, 2009 - Church and Curry: Combining Intrinsic and Extrinsic Typing
June 23, 2009 - The next 700 programming languages
June 16, 2009 - The Mechanical Evaluation of Expressions
June 2, 2009 - Types, Abstraction and Parametric Polymorphism
May 27, 2009 - Representing layered monads
May 12, 2009 - On the Meanings of the Logical Constants and the Justifications of the Logical Laws
May 5, 2009 - Branching vs. Linear Time: Semantical Perspective
April 14, 2009 - Display logic
March 24, 2009 - Contraction-Free Sequent Calculi for Intuitionistic Logic
March 17, 2009 - Proof search in Lax Logic
March 9, 2009 - Introduction to linear logic and ludics, part I
February 23, 2009 - Equality in lazy computation systems
February 16, 2009 - Syntactic Logical Relations for Polymorphic and Recursive Types
February 2, 2009 - What is a Sorting Function?
2008
October 27, 2008 - Classical Fω, orthogonality and symmetric candidates
October 6, 2008 - Call-by-name, call-by-value and the λ-calculus
September 29, 2008 - Definitional interpreters for higher-order programming languages
August 24, 2008 - Total Functional Programming
August 18, 2008 - From Axioms to Analytic Rules in Nonclassical Logics
June 18, 2008 - General Structural Operational Semantics through Categorical Logic
May 12, 2008 - Structural Logical Relations
April 7, 2008 - Combining Generic Judgments with Recursive Definitions
March 24, 2008 - Finally Tagless, Partially Evaluated
February 25, 2008 - Focusing and higher-order abstract syntax
February 18, 2008 - Engineering formal metatheory
February 11, 2008 - Clowns to the left of me, jokers to the right (pearl): dissecting data structures
2007
December 10, 2007 - A type system for recursive modules
November 26, 2007 - Principal Type Schemes for Modular Programs
October 15, 2007 - Inductive reasoning about effectful data types
October 8, 2007 - Extensible pattern matching via a lightweight language extension
September 30, 2007 - Practical Programming with Higher-Order Encodings and Dependent Types
September 24, 2007 - A certified type-preserving compiler from lambda calculus to assembly language
September 17, 2007 - Ott: effective tool support for the working semanticist
September 10, 2007 - Compiling with continuations, continued
July 7, 2007 - Tangible functional programming
June 11, 2007 - Beauty in the beast
April 30, 2007 - Compiling Comp Ling: practical weighted dynamic programming and the Dyna language
April 16, 2007 - Importing mathematics from HOL into Nuprl
April 9, 2007 - RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
March 5, 2007 - A generic normalisation proof for pure type systems
February 19, 2007 - Geometry of synthesis: a structured approach to VLSI design
February 11, 2007 - Lightweight fusion by fixed point promotion
February 5, 2007 - Assessing security threats of looping constructs
2006
December 11, 2006 - Abstract Predicates and Mutable ADTs in Hoare Type Theory
November 13, 2006 - Transactional events
October 23, 2006 - Relational Reasoning for Recursive Types and References
October 16, 2006 - A very modal model of a modern, major, general type system
October 2, 2006 - The missing link: dynamic components for ML
September 25, 2006 - Extensible programming with first-class cases
August 28, 2006 - A logic for parametric polymorphism
August 8, 2006 - Monadic concurrent linear logic programming
July 11, 2006 - Logic Programming with Focusing Proofs in Linear Logic
June 19, 2006 - Specifying distributed trust management in LolliMon
June 5, 2006 - Stratified type inference for generalized algebraic data types
May 29, 2006 - Jumbo λ-Calculus
May 22, 2006 - An Applicative Control-Flow Graph Based on Huet's Zipper
May 1, 2006 - An Overview of the Singularity Project
April 24, 2006 - Modular type classes
April 17, 2006 - Monadic regions
April 3, 2006 - Frame rules from answer types for code pointers
March 6, 2006 - A polymorphic modal type system for lisp-like multi-staged languages
February 27, 2006 - The next 700 data description languages
February 20, 2006 - Harmless advice
February 13, 2006 - Fast and loose reasoning is morally correct
February 6, 2006 - Formal certification of a compiler back-end or: programming a compiler with a proof assistant
January 30, 2006 - Institutions: abstract model theory for specification and programming
January 23, 2006 - A Tutorial on (Co)Algebras and (Co)Induction
2005
December 5, 2005 - Coinductive big-step operational semantics
November 21, 2005 - What are principal typings and what are they good for?
November 14, 2005 - A compositional natural semantics and Hoare logic for low-level languages
November 7, 2005 - A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework
October 24, 2005 - Combinators for Bi-Directional Tree Transformations: A Linguistic Approach to the View Update Problem
October 17, 2005 - A logical analysis of aliasing in imperative higher-order functions
October 10, 2005 - Contextual modal type theory
October 3, 2005 - Choice in Dynamic Linking
September 26, 2005 - Computational types from a logical perspective
September 19, 2005 - A judgmental reconstruction of modal logic
September 12, 2005 - On the Meanings of the Logical Constants and the Justifications of the Logical Laws
August 22, 2005 - Explicit substitutions
August 15, 2005 - Notions of computation and monads
August 8, 2005 - An expressive language of signatures
August 1, 2005 - An Explicit Substitution Notation in a lambdaProlog Implementation
July 18, 2005 - Flexible type analysis
July 11, 2005 - TypeCase: a design pattern for type-indexed functions
June 20, 2005 - Intensional polymorphism in type-erasure semantics
June 13, 2005 - Compiling polymorphism using intensional type analysis
May 30, 2005 - Mismatch
May 23, 2005 - The geometry of interaction machine
May 2, 2005 - Composable memory transactions
April 25, 2005 - Why Dependent Types Matter
April 18, 2005 - The Girard---Reynolds isomorphism (second edition)
April 11, 2005 - Types, Abstraction and Parametric Polymorphism
April 4, 2005 - From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple
March 21, 2005 - Definitional interpreters for higher-order programming languages
March 7, 2005 - A Logical Algorithm for ML Type Inference
February 28, 2005 - A unified theory of garbage collection
February 14, 2005 - The implementation of newsqueak
February 14, 2005 - Newsqueak: A Language for Communicating with Mice
February 7, 2005 - The reflexive CHAM and the join-calculus
January 24, 2005 - Existential Types for Imperative Languages
2004
December 6, 2004 - Relational parametricity and units of measure
October 25, 2004 - Macros as multi-stage computations: type-safe, generative, binding macros in MacroML
October 18, 2004 - Macros That Compose: Systematic Macro Programming
October 18, 2004 - An Advanced Syntax-Rules Primer for the Mildly Insane
October 11, 2004 - FreshML: programming with binders made simple
September 27, 2004 - Letters to the editor: go to statement considered harmful
September 20, 2004 - Destructors, finalizers, and synchronization
September 13, 2004 - An indexed model of recursive types for foundational proof-carrying code
August 16, 2004 - Subtyping is not a good ” match” for object-oriented languages
August 10, 2004 - A bisimulation for type abstraction and recursion
August 2, 2004 - Associated types with class
July 19, 2004 - A computational analysis of Girard's translation and LC
July 5, 2004 - Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
June 21, 2004 - A type-theoretical alternative to ISWIM, CUCH, OWHY
June 14, 2004 - Theorems for free!
June 1, 2004 - Parametric polymorphism and operational equivalence
May 17, 2004 - Syntactic type abstraction
April 26, 2004 - Contracts for higher-order functions
April 19, 2004 - Checking Interference with Fractional Permissions
April 5, 2004 - Alias Types for Recursive Data Structures
March 29, 2004 - A Symmetric Modal Lambda Calculus for Distributed Computing
March 22, 2004 - Fully reflexive intensional type analysis
March 15, 2004 - Flexible type analysis
March 8, 2004 - An Analysis of Girard's Paradox
March 1, 2004 - A theory of aspects
February 23, 2004 - Partial polymorphic type inference and higher-order unification
February 16, 2004 - MLF: raising ML to the power of system F