Advanced Programming Languages 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.
Introduction
On Understanding
Types, Data Abstraction, and Polymorphism (1985)
Luca Cardelli, Peter Wegner
Polymorphic Lambda Calculus
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
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
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
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
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
Pitfalls with references
Polymorphism
for Imperative Languages without Imperative Types (1993)
Andrew K. Wright
Existential
Types for Imperative Languages (2002)
Dan Grossman
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
Compiling Polymorphism
Using Intensional Type Analysis (1995)
Robert Harper, Greg Morrisett
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
Haskell Type Classes
How to make
ad-hoc polymorphism less ad-hoc (1988)
Philip Wadler, Stephen Blott
Polytypic programming & Generic Haskell
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
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
Generic Types in Java
Aspect-Oriented Programming
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
\renewcommand{\ttdefault}{cmtt}
\DeclareTextCommand{\textbraceleft}{OT1}{\texttt{\symbol{`\{}}}%}
\DeclareTextCommand{\textbraceright}{OT1}{\texttt{\symbol{`\}}}}
General tricks
\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}
\newcommand{\bracket}[]{\ensuremath{[\![#1]\!]}}
Home | Course Description | Assignments and Grading | Schedule | Last Modified: 09.12.02