David Binder

Stream: new members

[David Binder]

Hello everyone! I have been hanging around here for a while, but not actively posting. I am a PL and type theory researcher and postdoc at the University of Kent. I have a lot of experience using Rocq to formalize type theory papers, and I am learning my way around using Lean. Two public work in progress Lean projects I am working on are https://github.com/BinderDavid/veriflex , a verified lexer generator using Brzozowski derivatives, and https://github.com/BinderDavid/haskell-spec a specification of the Haskell 2010 type system based on a paper by Karl-Filip Faxen. :wave:

[Yaël Dillies]

:wave: What a great lastname you have!

[David Binder]

Haha, thanks :)

[Kyle Miller]

Neat, I've thought it would be fun to implement a Brzozowski-derivative-based parser in Lean before.

It would be cool if there were a way to apply a Futamura projection (i.e. partially evaluate) the lexer to specialize it to a particular regular expression, and get a recursive function. I know derivatives are a way to create a nondeterministic state machine, but maybe it's possible to avoid the state machine construction and use only program transformations.

[David Binder]

Yes, the performance without any sort of specialization is probably not good at the moment. My main objective is to try to implement a verified Haskell parser which can be simultaneously used as a specification. If I find the spare time I will try to implement a parser for indentation-sensitive context-free grammars (https://michaeldadams.org/papers/layout_parsing/) as well :)