Advanced Programming Languages CIS 670 Fall 2002 Resources and References

The papers and books listed on this page are places to look for more information about the lecture topics. Almost all of them are available online. Skimming through them may also help you find an interesting topic for your semester project. I will be updating this list throughout the semester.

Papers

1. Introduction

   • On Understanding Types, Data Abstraction, and Polymorphism (1985)
     Luca Cardelli, Peter Wegner

2. Polymorphic Lambda Calculus

   • Lambda Calculi with Types (1992)
     Henk Barendregt

3. Encoding of inductive types

   • Automatic synthesis of typed Lambda-programs on term algebras (1985)
     Corrado Böhm and Alessandro Berarducci
     Theoretical Computer Science, 39(2/3):135-154, August 1985.

   • Proofs and Types (1989), ch. 11
     Girard, Lafont, Taylor
     Cambridge University Press

4. Existential Types

   • Abstract types have existential type (POPL 1985)
     John Mitchell, Gordon Plotkin

   • Typed Closure Conversion for Recursively-Defined Functions (1997)
     Greg Morrisett, Robert Harper

   • Abstract types and the dot notation (1990)
     Luca Cardelli, Xavier Leroy

5. Termination/Strong Normalization of System F
   • Parametricity and Variants of Girard's J Operator (1994)
     Robert Harper, John C. Mitchell
     
     
   • On Girard's "Candidates de Reductibilite" (1990)
     Jean Gallier
     Piergiorgio Odifreddi, editor, Logic and Computer Science, number 31 in APIC Studies in Data Processing, pages 123--203. Academic Press, 1990.
     
     
6. Curry-Howard Isomorphism/Parametricity

   • Proofs are Programs: 19th Century Logic and 21st Century Computing (2000)
     Philip Wadler

   • Theorems for Free! (1989)
     Philip Wadler

   • The Girard-Reynolds Isomorphism (2001)
     Philip Wadler

7. Higher-order types

   • From Fast Exponentiation to Square Matrices: An Adventure in Types (1999)
     Chris Okasaki.

   • Phantom types and subtyping (2002)
     M. Fluet, R. Pucella.

   • Metacircularity in the polymorphic lambda-calculus (1991)
     Frank Pfenning and Peter Lee.
     Theoretical Computer Science 89 (1991) 137-159
     

8. Type inference

   • A Theory of Type Polymorphism in Programming (1978)
     Robin Milner.
     JCSS 17(3): 348-375 (1978)

   • Local type inference (1998)
     Benjamin C. Pierce, David N. Turner

9. Pitfalls with references

   • Polymorphism for Imperative Languages without Imperative Types (1993)
     Andrew K. Wright

   • Existential Types for Imperative Languages (2002)
     Dan Grossman

10. Dynamic types

    • Dynamic Typing in a Statically Typed Language (1989)
      Martín Abadi, Luca Cardelli, Benjamin Pierce, Gordon Plotkin

    • Encoding Types in ML-like Languages (1998)
      Zhe Yang

11. Compiling Parametric Polymorphism
    
    
• Unboxed Objects and Polymorphic Typing (1992)
  Xavier Leroy

• Compiling Polymorphism Using Intensional Type Analysis (1995)
  Robert Harper, Greg Morrisett

• Flexible Representations Analysis (1997)
  Zhong Shao
  
  
• The effectiveness of Type-Based Unboxing (1997)
  Xavier Leroy
  
  
• Compiling Functional Languages, part 4 (lecture, 2002)
  Xavier Leroy
  

12. More on intensional polymorphism

    • Intensional Polymorphism in Type-Erasure Semantics (1998)
      Karl Crary, Stephanie Weirich, Greg Morrisett

    • A Language for Flexible Type Analysis (1999)
      Karl Crary, Stephanie Weirich

    • Fully-Reflexive Intensional Type Analysis (2000)
      Valery Trifonov, Bratin Saha, Zhong Shao

13. Haskell Type Classes

    • How to make ad-hoc polymorphism less ad-hoc (1988)
      Philip Wadler, Stephen Blott

    • Type classes in Haskell (1996)
      Cordelia Hall, Kevin Hammond, Simon Peyton Jones, Philip Wadler
      
      
    • A Gentle Introduction to Haskell.
      Paul Hudak, John Peterson, Joseph Fasel. Revised June, 2000 by Reuben Thomas. See section: Type Classes and Overloading.
      
      
    • A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism (1993)
      Mark Jones
      
      
    • Type classes with functional dependencies (2000)
      Mark Jones
      
      
    • Functional Logic Overloading (2002)
      Martin Gasbichler, Matthias Neubauer, Michael Sperber, Peter Thiemann

14. Polytypic programming & Generic Haskell

    • Polytypic values possess polykinded types (2000)
      Ralf Hinze
    
    
15. Dependent Types
    
    • Lambda Calculi with Types (1992)
      Henk Barendregt
    • Cayenne, A Language with Dependent Types (1998)
      Lennart Augusston
      
    • Dependent Types in Practical Programming (1998)
      Hongwei Xi
      
      
16. Overloading/Multi-method dispatch

    • Common Lisp Object System specification X3J13. (1988)
      Daniel G. Bobrow, Linda G. DeMichiel, Richard P. Gabriel, Sonya E. Keene, Gregor Kiczales, and David A. Moon.

    • Typechecking and Modules for Multi-Methods (1995)
      Craig Chambers, Gary T. Leavens

    • A Calculus for Overloaded Functions with Subtyping (1995)
      Castagna,Ghelli, Longo

17. Named vs. Structural Types

    • Type Dispatch for Named Hierarchical Types (1999)
      Neal Glew

    • Scrap your Boilerplate: a practical design pattern for generic programming (2002)
      Simon Peyton Jones and Ralf Lämmel

18. Generic Types in Java

19. Aspect-Oriented Programming

Books and Lecture Notes

Types and Programming Languages (2001)
Benjamin Pierce
MIT Press

Programming Languages: Theory and Practice (Book Draft, 2002)
Robert Harper

Lectures on the Curry-Howard Isomorphism (1998)
M H Sørensen and P Urzyczyn.

The Lambda Calculus: Its Syntax and Semantics (1984)
Henk Barendregt

Type Theory and Functional Programming (1991)
Simon Thompson

LaTeX

1. proof.sty - inference rules
2. code.sty - verbatim-like environment for writing code mixed with math symbols
   • I had to add the following text to make the braces come out in the right font

     \renewcommand{\ttdefault}{cmtt}
     \DeclareTextCommand{\textbraceleft}{OT1}{\texttt{\symbol{`\{}}}%}
     \DeclareTextCommand{\textbraceright}{OT1}{\texttt{\symbol{`\}}}}

3. General tricks

   • Change < > to be angle brackets

     \mathchardef\lt="313C  % Use \lt for <
     \mathchardef\gt="313E  % Use \gt for >
     %% use \ltgtforanglebrackets command to redefine <,> to stand for \langle, \rangle
     \newcommand{\ltgtforanglebrackets}{\mathcode`<="4268 \mathcode`>="5269}

   • Semantic brackets

      \newcommand{\bracket}[]{\ensuremath{[\![#1]\!]}}

Home | Course Description | Assignments and Grading | Schedule | Last Modified: 09.12.02