Talk:Dependently Typed Binary Lambda Calculus

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

[2] https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634