2026-09-19T21:37:18Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/81573 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Kamin, Samuel N. Harrison, William Lawrence 2015-09-25T20:19:15Z 2015-09-25T20:19:15Z 10000-01-01 2001 2001 This thesis explores the construction and correctness of modular compilers. Modular compilation is a compiler construction technique allowing the construction of compilers for high-level programming languages from reusable compiler building blocks. Modular compilers are defined in terms of denotational semantics based on monads, monad transformers, and a new model of staged computation called metacomputations. A novel form of denotational specification called observational program specification and related proof techniques are developed to assist in modular compiler verification. It will be demonstrated that the modular compilation framework provides both a level of modularity in compiler proofs as well as a useful organizing principle for such proofs. Made available in DSpace on 2015-09-25T20:19:15Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 3017092.pdf: 7394299 bytes, checksum: 55104b8b7463ee6f228034c33fe858ec (MD5) Previous issue date: 2001 Embargo set by: Seth Robbins for item 82854 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs U of I Only 283 p. Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2001. http://hdl.handle.net/2142/81573 (MiAaPQ)AAI3017092 eng Computer Science Modular Compilers and Their Correctness Proofs text Computer Science Computer Science University of Illinois at Urbana-Champaign Dissertation Ph.D.