In our inaugural episode, we speak with Peter Dybjer from Chalmers University of Technology. Peter has made significant contributions to type theory, including inductive families, induction-recursion, and categorical models of dependent types. He is generally interested in program correctness, programming language semantics, and the connection between mathematics and programming. Today, we will talk about the relationship between QuickCheck-style testing and proofs and verification in type theory.
- On Full Abstraction for PCF: I, II, and III
- A Concrete Presentation of Game Semantics
- Algorithmic Game Semantics and its Applications: Final Report