Jason Reich
  • Member for 11 years, 5 months
  • Last seen more than 3 years ago
Compiler correctness proofs
7 votes

Graham Hutton has a small example in his book "Programming in Haskell" which is a great place to start. I also have a few mechanised proofs (various logics) of the McCarthy-Painter compiler in a ...

View answer
Relationship between contracts and dependent typing
6 votes

Both contracts and types allow you to represent Hoare-style (pre/post condition) specifications on functions. Both can be checked either statically at compile time or dynamically at runtime. ...

View answer