Typer: An infix statically typed Lisp

Stefan Monnier

I'll present the current design of the programming language Typer which tries to combine Lisp-style syntactic flexibility and Scheme-style minimalism together with dependent types to make a proud member of the ML/Haskell family of programming languages. I'll of course go over the syntactic aspects of the design, which I already presented at the ML-workshop, but will spend more time on the rest of the design more closely related to type systems and proof assistants, including presenting parts of the metatheory that still dearly needs to be clarified and proven.