Source code of three interpreters for the ET language, also known as IPL:
-
The original SML implementation, by Tomasz Wierzbicki, dated 19 November 1993
-
An SML implementation, by Marek Łach, dated 6 November 1998
-
An OCaml implementation, by Michał Moskal, dated 5 November 2004
Includes all available literature.
- Z. Spławski (1988) “Teoriodowodowe podejście do programów funkcyjnych i typów danych”
- Z. Spławski (1991) “Proof-theoretic approach to automatic synthesis of polymorphic programs”
- Z. Spławski (1993) “IPL by examples”
- T. Wierzbicki (1993) “On the implementation of IPL”
- Z. Spławski (1993) “Proof-theoretic approach to inductive definitions in ML-like programming language vs. second-order lambda calculus”
- Z. Spławski (1995) “Proving equalities in λ→ with positive (co-)inductive data types”
- Z. Spławski (1996) “Subtyping λ→ with positive (co-)inductive data types”
- Z. Spławski (1997) “Proving equalities in second-order lambda calculus with inductive and recursive types”
- M. Łach (1998) “Teoria typów z definicjami indukcyjnymi jako język programowania”
- Z. Spławski (1998) “Continuations in λ→ with positive (co-)inductive data types”
- Z. Spławski (1999) “Interdefinability of positive coinductive types with corecursors”
- P. Urzyczyn (1999) “The Curry-Howard isomorphism: Remarks on recursive types”
- Z. Spławski, P. Urzyczyn (1999) “Type fixpoints: iteration vs. recursion”
- Z. Spławski (2002) “Defining recursors by solving equations in second-order lambda calculus”
Packaged by Miëtek Bak.