Type-Refinements.info

Software

SML CIDRE: Rowan Davies' datasort refinement typechecker for full Standard ML.
Stardust: an implementation of datasort refinement/index refinement/intersection/union typechecking for a subset of SML; not yet public, but there are a few cryptic examples that appeared in my dissertation. (You can see the status of of a project of the same name... ;-)

Talks

Joshua Dunfield, Refined typechecking with Stardust (PLPV '07, Freiburg), October 2007 (PDF file for onscreen viewing)
Joshua Dunfield, Applying type refinements: a tutorial, May 2005 (PDF file for onscreen viewing)

(Rest of section to be constructed.)

Theses

(In reverse chronological order.)

Joshua Dunfield, A unified system of type refinements, August 2007
Rowan Davies, Practical refinement-type checking, May 2005
Hongwei Xi, Dependent types in practical programming, 1998
Tim Freeman, Practical refinement-type checking, 1994

Papers

(Section to be constructed; in the meantime, look at the list of papers for Bob Harper's 2003 seminar on type refinements.)

People

Some researchers in type refinements and related areas (reverse alphabetical):

Hongwei Xi (BU)
David Walker (Princeton)
Susmit Sarkar (CMU)
Frank Pfenning (CMU)
Yitzhak Mandelbaum (~~Princeton~~ AT&T Research)
Robert Harper (CMU)
Joshua Dunfield (~~CMU~~ McGill)
Rowan Davies (Western Australia)

Links

CMU Triple Project (Type Refinements in Programming Languages)

type-refinements.info hosted by sigpie.org
Powered by

Puffy

OpenBSD

Joshua Dunfield

Last modified: Mon Oct 15 11:16:07 EDT 2007