Lab for Automated Reasoning and Analysis LARA

Lecture 15: Overview of Some Additional Topics

Elements of Garbage Collection (GC)

References

Call-by-Name and Lazy Evaluation

References

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

Parallelism

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
 
© EPFL 2018 - Legal notice