Formal proof of correctness Ö

• Search Algorithms in Type Theory

  • Jim Caldwell, Ian Gent, Judith Underwood
  • Theoretical Computer Science, 232 (2000), 255-290

• Ok Iíll skip it but Ö.

  • Ö it contains a formal proof plus extracted program

Previous slide

Next slide

Back to first slide

View graphic version