Lab for Automated Reasoning and Analysis LARA

Lecture 15: Overview of Some Additional Topics

Elements of Garbage Collection (GC)


Call-by-Name and Lazy Evaluation


Languages with Non-Determinism

Software Synthesis

Correctness and Compilers

  • Compcert - a compiler formally proved correct using the Coq interactive proof assistant
  • Translation Validation - compiler emits, for each individual program, an independently verifiable certificate that the compilation was correct


Some Useful Compiler Infrastructures

Your own compiler: the big advantage is that you understand it

Other recent open-source infrastructures:

cc09/lecture_15.txt · Last modified: 2009/12/16 16:29 by vkuncak