We are currently working on new rules for what content should and shouldn't be allowed on this website, and are looking for feedback! See Esolang:2026 topicality proposal to view and give feedback on the current draft.
Talk:Dependently Typed Binary Lambda Calculus
Jump to navigation
Jump to search
This is closely related to the implementation of the Calculus of Constructions (CoC) in binary lambda calculus in [1] also discussed in [2].
[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/loader.lam