• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
    • Loop$-primer
    • Operational-semantics
      • Operational-semantics-3__annotated-bibliography
        • Bib::bhmy89
        • Bib::liu06
        • Bib::bm96
        • Bib::plotkin04b
        • Bib::bgm90
        • Bib::hkms17
        • Bib::bkm96
        • Bib::moore15
        • Bib::bh99
        • Bib::wilding93
        • Bib::plotkin04a
        • Bib::moore03b
        • Bib::mp02
        • Bib::moore19
        • Bib::manolios00
        • Bib::flatau92
        • Bib::hb92
        • Bib::bm05
        • Bib::goel16
        • Bib::bm73
        • Bib::ghk17
        • Bib::wilding92
        • Bib::moore17
        • Bib::moore96
        • Bib::ghkg14
        • Bib::yu92
        • Bib::hunt85
        • Bib::boh03
        • Bib::mmrv06
        • Bib::bm80
        • Bib::bh97
        • Bib::moore99b
        • Bib::moore14
        • Bib::rm04
        • Bib::by96
        • Bib::sawada00
        • Bib::mccarthy62
        • Bib::bm79
        • Bib::moore99a
        • Bib::sh98
        • Bib::rhmm07
        • Bib::kmm00a
        • Bib::ghk13
        • Bib::moore03a
        • Bib::hk12
        • Bib::mp67
        • Bib::young88
        • Bib::bm97
        • Bib::moore73
        • Bib::kmm00b
        • Bib::bevier87
      • Operational-semantics-1__simple-example
      • Operational-semantics-2__other-examples
      • Operational-semantics-5__history-etc
      • Operational-semantics-4__how-to-find-things
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Operational-semantics-3__annotated-bibliography

Bib::young88

W. D. Young, A Verified Code Generator for a Subset of Gypsy (ftp://ftp.cs.utexas.edu/pub/boyer/diss/young.pdf), University of Texas at Austin, Ph.D. dissertation, 1988.



Relevance: a verified compiler (from a small Pascal-like subset to an assembly language) and a component of the CLI Verified Stack

———

The verified compiler used in the CLI Verified Stack as reported in bib::bhmy89 is described here. By the way, we could not find the original Nqthm script for this effort, but the complete script is included in Appendix B of the linked pdf file above, pages 206-860.