Topics in Programming Languages: Types and Contracts

CMSC 32001 (Spring 2015) | Ravi Chugh | MW 3:00-4:20pm | Ryerson 276


[M 03.30] Intro and Planning
[W 04.01] Depending on Types (Stephanie Weirich, ICFP 2014 Keynote)

[M 04.06] no class
[W 04.08] Operational Semantics

[M 04.13] no class (ESOP)
[W 04.15] no class (ESOP)

[M 04.20] More Big-Step Semantics; Recursion
[W 04.22] Applying "Design by Contract" (Meyer, IEEE 1992); Contracts... (Findler and Felleisen, ICFP 2002)

[M 04.27] Gradual Typing for Functional Languages (Siek and Taha, SFP 2006)
[W 04.29] Hybrid Type Checking (Flanagan, POPL 2006)

[M 05.04] Threesomes, With and Without Blame (Siek and Wadler, POPL 2010)
[W 05.06] Rust (Joe)

[M 05.11] Swift/T (Wozniak et al, CCGrid 2013); Compiler Techniques... (Armstrong et al, SC 2014)
[W 05.13] Certified Gradual Programming in Coq (Eric Tanter)

[M 05.18] Alias Types for Recursive Data Structures (Walker and Morrisett, TIC 2001)
[W 05.20] Adoption and Focus (Fahndrich and DeLine, PLDI 2002)

[M 05.25] no class (Memorial Day)
[W 05.27] Compositional and Decidable Checking for Dependent Contract Types (Knowles and Flanagan, PLPV 2009)

[M 06.01] Nested Refinements (Chugh et al, POPL 2012)
[W 06.03] Dependent JavaScript (Chugh et al, OOPSLA 2012)

Some More Papers

Well-Typed Programs Can't Be Blamed (Wadler and Findler, ESOP 2009)
Typed-Based Data Structure Verification (Kawaguchi et al, PLDI 2009)
Abstract Refinement Types (Vazou et al, ESOP 2013)
Confined Gradual Typing (Allende et al, OOPSLA 2014)
Alias Types (Walker et al, ESOP 2000)
Checking and Inferring Local Non-Aliasing (Aiken et al, PLDI 2003)
Logical Types for Untyped Languages (Tobin-Hochstadt and Felleisen, ICFP 2010)