Datatypes in L2

Nick Chapman, Simon Finn, Michael P. Fourman

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We describe the axiomatisation of a subset of Standard ML's datatypes in L2 (the LAMBDA Logic). The subset includes parameterisation and mutual recursion but has restrictions on the use of function type construction. We sketch a set-theoretic model for these datatypes. Finally, we briefly discuss the relationship between L2's datatypes and datatypes in HOL.
Original languageEnglish
Title of host publicationHigher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings
Number of pages16
ISBN (Electronic)978-3-540-48803-3
ISBN (Print)978-3-540-58450-6
Publication statusPublished - 1994

Fingerprint Dive into the research topics of 'Datatypes in L2'. Together they form a unique fingerprint.

Cite this