Datatypes in L2

Nick Chapman, Simon Finn, Michael P. Fourman

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

Abstract

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
PublisherSpringer-Verlag
Pages128-143
Number of pages16
Volume859
ISBN (Electronic)978-3-540-48803-3
ISBN (Print)978-3-540-58450-6
DOIs
Publication statusPublished - 1994

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

Cite this