A minimal typed lambda-calculus with singleton types and Pi-types is introduced. Some basic meta-properties are proved and it is given a PER semantics.David Aspinall.
Click here to return to my papers page.
David R. Aspinall, email david.aspinall@ed.ac.uk.