Open invitation: If you are learning Agda or Martin-Löf type theory and wish to talk about it or related matters, contact me and I will try to help to the best of my ability.
5
13
79
Conversation
Do you know of any formulations of a typed lambda-I calculus (lambda calculus with no vacuous binding allowed) in Agda?
4
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
The proof system for what I'm after is pretty straightforward; I'm hoping to find a treatment in Agda, though. Do you know if something like this general calculus has been put together in Agda?
1
2
I have a feeling I've seen some linear lambda calculi floating around github… maybe those might be interesting to check out? Not really an expert in Agda though, so I'm not sure what complications people normally run into when doing this kind of work.
1
1
And yeah, not sure what differences there would be between those and what you would be interested in, with lambda-I… (not being an expert in logic haha).
1
Seems a little more light on the ground than I had remembered: github.com/search?q=linea (not sure if it is just my keywords though).
Maybe I had seen some stuff on third-party gitlab instances. 😬
1
2
Some of that looks like it might be useful!
1
Oh cool! Glad it was not all in vain!