Type Inference Logics
summary
Shows how to verify practical, imperative-style, constraint-based type inference that emits elaborated terms by separating constraint generation (implemented as free-monad constraint generators) from solving, formalizing semantics with a WP/WLP program logic and mechanizing everything in Coq mechanization with Iris proof automation. Delivers a machine-checked implementation, proves soundness and completeness for three elaborating inferencers for the simply typed lambda calculus with Booleans, extracts a tiny Haskell implementation, and ships reproducible artifacts.
AI-written summary · about
chapters (11)
- 0:00Type inference logics intro
- 1:01Constraint-based type inference
- 2:26GHC’s type inference
- 3:28Semantic constraints concept
- 4:56Monad for constraint generation
- 6:22Proving typing correctness
- 8:06Soundness and completeness
- 10:16Lightning round
- 12:06Kripke-indexed constraints
- 13:13Mechanized proofs extraction
- 14:17Question and answer session
related talks
16mA Hoare-Logic Style Refinement Types Formalisation
45mLogic Meta Programming for Functional Languages
01h 34mFormal Logic Undressed
01h 02mType Inference in GHC
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
52mType Theory and its Meaning Explanations
19mIll-Typed Programs Don't Evaluate
22mA Calculus of Inductive Linear Constructions