(original) (raw)

Programming in Higher-Order Logic

ANU Logic Summer School, 7 -- 18 December 2009

Slides

Lecture 1 Lecture 2, Lecture 3, Lecture 4, Lecture 5. Course notes

Codes

All codes used in the course are written in lambda-Prolog.

• difflist.sig, difflist.mod: Difference lists.
• flist.sig,flist.mod: Function lists.
• funs.sig,funs.mod: Passing functions as arguments.
• germs.sig,germs.mod: `Germs in a jar'. A simple example of the use of implication in program clauses.
• minifp.sig,minifp.mod: An interpreter for a mini functional programming language.
• basic.sig,basic.mod: Some basic examples of first-order datatypes.
• persons.sig,persons.mod: An example of higher-order programming.
• preds.sig,preds.mod: Passing predicates as arguments.
• prenex.sig,prenex.mod: Prenex normal form transformation.
• reverse.sig,reverse.mod: Reversing a list.
• streams.sig,streams.mod: Encoding infinite streams. They have been tested using theTeyjus compiler for lambda-Prolog.

How to run the codes

Compile:

$ tjcc difflist
$ tjlink difflist

and run:

$ tjsim difflist