A Virtual Machine for a Type-omega Denotational Proof Language

Title: en_US A Virtual Machine for a Type-omega Denotational Proof Language
Creator: en_US III, Teodoro Arvizo
Date: 2004-10-20T20:29:40Z
Date Available: 2004-10-20T20:29:40Z
Date Issued: en_US 2002-06-01
Identifier: en_US AITR-2002-004
uri: http://hdl.handle.net/1721.1/7092
Abstract: en_US In this thesis, I designed and implemented a virtual machine (VM) for a monomorphic variant of Athena, a type-omega denotational proof language (DPL). This machine attempts to maintain the minimum state required to evaluate Athena phrases. This thesis also includes the design and implementation of a compiler for monomorphic Athena that compiles to the VM. Finally, it includes details on my implementation of a read-eval-print loop that glues together the VM core and the compiler to provide a full, user-accessible interface to monomorphic Athena. The Athena VM provides the same basis for DPLs that the SECD machine does for pure, functional programming and the Warren Abstract Machine does for Prolog.
Extent: en_US 106 p.; 2935187 bytes; 816842 bytes
Format: application/postscript; application/pdf
Language: en_US
Relation: en_US AITR-2002-004
Subject: en_US AI; en_US virtual machine; en_US SECD; en_US SECD machine; en_US denotational proof language; en_US Athena