A non-strict polymorphic , functional language by Jon Fairbairn jf@cl.cam.ac.uk .
Ponder's type system is unusual. It is more powerful than the Hindley-Milner type system used by ML and Miranda and extended by Haskell . Ponder adds extra recursive 'mu' types to those of Girard's System F , allowing more general recursion . Surprisingly, the type system and type inference algorithm are still not completely understood.
["Ponder and its Type System", J. Fairbairn, TR 31, Cambridge U Computer Lab, Nov 1982].
[J. Fairbairn, "Design and Implementation of a Simple Typed Language based on the Lambda-Calculus", Technical Report No. 75, Computer Laboratory, University of Cambridge, May 1985].
[J. Fairbairn, "A New Type-Checker for a Functional Language", Technical Report No. 53, Computer Laboratory, University of Cambridge, 1984].
[J. Fairbairn, "Some Types with Inclusion Properties in \forall, \rightarrow, \mu", Technical Report No. 171, Computer Laboratory, University of Cambridge, Jun 1989].
[Valeria C. V. de Paiva, "Subtyping in Ponder (Preliminary Report)", Technical Report No. 203, Computer Laboratory, University of Cambridge, Aug 1990].