Pure2
This page is about Pure2, an interpreter for finite, functional pure type systems.

Pure2 is a simple interpreter for specifying (finite (finite sort, axiom, and rule sets), functional (singly-sorted)) PTS's and tinkering with them. One can posit inhabitants for particular types, query the interpreter for alpha-equivalence or beta-convertibility of pseudo-terms, define simple abbreviations / macros, normalise and type-check pseudo-terms.

I implemented the language as part of studying for my oral qualifying examination, as a tool for testing out some ideas, to convince myself that I understood several topics, and as a language to use for the presentation at the examination. I despise seeing talks with code in hypothetical languages that's never been run, so I wanted to be sure that everything that I showed was executable (and had been type-checked).

Pure2 is implemented in CamlTrax, my dialect of OCaml, and incorporates code from Braque (my evolving-typed language), LamLang / Morphine (my little System-F-based functional language), and Pure (Pure2's predecessor, which I used for several talks at the PL group). The syntax was modelled after (a subset of) Agda's. Compiling the interpreter will require (at least) the following tools: CamlTrax (preprocessor), DypGen (parser generator), OCamlLex (lexer generator), ExtLib (set of libraries), and FindLib (library). To run the interpreter effectively, it would be helpful to use RLWrap, LEdit, or Emacs.

• 2008-05-03–Uploaded source code and binary distributions of Pure2. There's also a file describing the syntax that the interpreter accepts.
• 2008-05-01–Created this page. Source code plus documentation to come soon.

• Description of Pure2 syntax and commands (text)
• Simple example file (Pure2 source)
• Pure2 source code (OCaml, CamlTrax, DypGen, and OCamlLex source)
• Pure2 for GNU/Linux x86 (binary only)
• Pure2 for OSX PPC (binary only; this works on x86 OSX also)
• Pure2 for Windows XP x86 (binary and required dynamic library)

Well, there's really no more information available for the time being, sorry! Please check back soon, though, or e-mail me if you have specific questions.