LGM on LADL proof theory

[dckc]

On Apr 22, he referred me to https://github.com/rchain/pi4u/tree/master/AFreshProofTheoryForLADL :

That’s behind our current work by about 2 weeks. We’re incorporating this paper. That allows us to eliminate most of the contextualized resourced theory, but it has the consequence of adding meta-variables to our type judgments.

i am evaluating Kiama as an input format for the theories LADL takes as input by implementing the rho-combinator paper. The code for this implementation is here.

[dckc]

update: https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html