New examples: code synthesis and evaluation through reflection
A mechanised soundness proof for a reflective theorem prover.