ACM Logo ACM Logo

TLDI 2012

The Seventh ACM SIGPLAN Workshop on

Types in Language Design and Implementation


Philadelphia, PA, USA

Saturday, January 28, 2012

To be held in conjunction with POPL 2012



Welcome to TLDI 2012

The role of types and proofs in all aspects of language design, compiler construction, and software development has expanded greatly in recent years. Type systems, type analyses, and formal deduction have led to new concepts in compilation techniques for modern programming languages, verification of safety and security properties of programs, program transformation and optimization, and many other areas. In light of this expanding role of types, the Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2012) aims to bring together researchers from around the globe to share exciting new ideas and results in this area. This year's workshop is the tenth in a series of international workshops, originating in 1997 as the Workshop on Types in Compilation (TIC).

Important: This year we are introducing a significant change to the workshop organization. There will now be two distinct submission categories: full papers (with a published proceedings, as always) and 2-page proposals for talks on more speculative or unfinished work. The aim is to foster a more informal atmosphere while maintaining the TLDI tradition of excellent presentations of polished technical work.

Submission Site

Here. (Please see the CFP for detailed instructions.)


Via the POPL 2012 registration site.

Workshop Program

Session 1: 9:00 - 10:00

Invited talk
Towards Concurrent Type Theory
Frank Pfenning (Carnegie Mellon University)

Session 2: 10:30 - 11:50

Exact Type Parameterization and ThisType Support
Hyunik Na, Sukyoung Ryu, and Kwangmoo Choe (KAIST)

Types for Relaxed Memory Models
Matthew Goto, Radha Jagadeesan, Corin Pitcher, and James Riely (DePaul University)

Towards a Formal Semantics for a Structurally Dynamic Non-causal Modelling Language
John Capper and Henrik Nilsson (University of Nottingham)

A Technique for Proving Subtyping Completeness, with an Application to Iso-recursive Types (short paper)
Jay Ligatti (University of South Florida)

Session 3: 2:00 - 3:30

Invited talk
Semantics for Graphical User Interfaces
Neelakantan Krishnaswami (MPI-SWS)

Towards Practical Runtime Type Instantiation (short paper)
Karl Naden (Carnegie Mellon University)

Safe Incremental Type Checking (short paper)
Matthias Puech (University of Bologna, PPS Team πr²) and Yann Regis-Gianas (PPS Team πr²)

Session 4: 4:00 - 5:20

Giving Haskell a Promotion
Brent A. Yorgey (Unversity of Pennsylvania), Stephanie Weirich (University of Pennsylvania), Julien Cretin (INRIA), Simon Peyton Jones (Microsoft Research), Dimitrios Vytiniotis (Microsoft Research), and José Pedro Magalhães (Utrecht University)

Static Lock Capabilities for Deadlock Freedom
Colin S. Gordon, Michael D. Ernst, and Dan Grossman (University of Washington)

Type Systems for Dummies
Andrea Asperti and Ferruccio Guidi (University of Bologna)

Row-based effect types for database integration and concurrency
Sam Lindley and James Cheney (University of Edinburgh)

Important Dates

Submission deadline October 10, 2011 (Monday), 11:59PM, EDT
Notification November 10, 2011 (Thursday)
Workshop January 28, 2012 (Saturday)



Program Chair:


Benjamin C. Pierce
University of Pennsylvania
bcpierce atsign cis dot upenn dot edu


Program Committee: 

Jonathan Aldrich CMU
Adam Chlipala MIT
Pierre-Malo Denielou Imperial College
Kathleen Fisher Tufts University
Chris Hawblitzel Microsoft Research (Redmond)
Dan Licata CMU
Greg Morrisett Harvard University
Benjamin C. Pierce University of Pennsylvania
Dimitrios Vytiniotis Microsoft Research (Cambridge)


Steering Committee: 

Amal Ahmed Indiana University
Nick Benton Microsoft Research, Cambridge
Derek Dreyer MPI-SWS
Andrew Kennedy Microsoft Research, Cambridge
Francois Pottier INRIA Paris-Rocquencourt
Stephanie Weirich University of Pennsylvania