Is There a Future for a Formally Specified Haskell Report
summary
Project implements a verified frontend in Lean that covers Unicode lexing, indentation-sensitive tokenization, renaming, fixity resolution and grouping of mutually recursive declarations, and aims to produce a machine-checked AST; it formalizes K‑F Faxen’s declarative typing by translating its 60+ page rules into Lean and plans an algorithmic typechecker proved correct against it. Uses principled parsing for indentation-sensitive languages, adapts verified-lexer techniques, has working specs but no wide conformance test suite yet.
AI-written summary · about
chapters (20)
- 0:00Haskell origins and talk intro
- 1:09Whitespace in programming
- 4:01Haskell's informal report issues
- 7:16Formal language specs today
- 9:04Verified compilers for Haskell-like
- 12:17Mechanizing vs proving meta-theory
- 14:04Verified frontend for Haskell 2010
- 18:16Phased static semantics
- 22:15Lexical syntax and indentation
- 27:13Indentation-sensitive parsing
- 29:48Name resolution challenges
- 31:58Type system and type classes
- 35:08Formal spec as source of truth
- 36:12Vision for Haskell's formal report
- 38:20Mechanizing Haskell 2010 modules
- 41:30Haskell 2010 scope and limits
- 42:54Simplifying Haskell for mechanization
- 44:18Compiler conformance testing
- 45:43Crowdsourcing formalization
- 46:26Closing remarks
related talks
30mTrustworthy Formal Natural Language Specifications
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
01h 05mAll the Languages Together
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
34mLiquid Haskell: Verification with Refinement Types
42mFunctional interpreters and you
20mDeveloping a Monadic Type Checker for an Object-Oriented Language