New Theorem Prover Support

• Work on translation of Haskell to Martin-Löf Type Theory

  • Good match!
  • Translation guided by types
    • Polymorphism ? explicit type parameters
  • Prove properties of Haskell programs in the proof editor Alfa
  • Check termination of Haskell programs

Previous slide

Next slide

Back to first slide

View graphic version