4 ms·

This is really cool. I've been doing something in a similar vein at https://github.com/sgodwincs/lamda_calculus_formalizations https://github.com/sgodwincs/lamd

This is really cool. I've been doing something in a similar vein at https://github.com/sgodwincs/lamda_calculus_formalizations https://github.com/sgodwincs/lamda_calculus_formalizations, though the difference being I'm using Lean and trying to prove certain properties of the languages (type safety, normalization, etc.). Of course, compared to unification and stuff you have, I only have very simple additions like natural numbers and binary product types (though the proofs still are hard for me!). Working on finite product types now and it's an absolute pain to even define it in a way that Lean likes.

solomonb 3y ago
Your project is cool too! I haven't tried Lean yet but have done some similar formalization in Agda. I went with Haskell as my meta-language because I'm specifically trying to focus on language implementation rather then formal analysis and proofs. I have everything from the README other then linear types, row polymorphism, and case-trees implemented outside the repo (and some in the main/old folder). I haven't gotten them into the repo yet because I want to make sure the implementations are succinct and decently documented. I want to move onto a 1lab style presentation with substantially more documentation at a later date.