Skip to main content
added 384 characters in body
Source Link
Ohad Kammar
  • 2.7k
  • 23
  • 28

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction.

The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and Eisenbach's Zeno and Vytiniotis, Peyton-Jones, Claessen, and Rosen's Halo.

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction.

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction.

The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and Eisenbach's Zeno and Vytiniotis, Peyton-Jones, Claessen, and Rosen's Halo.

Source Link
Ohad Kammar
  • 2.7k
  • 23
  • 28

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction.