[MOVED] Charlag is a user on mastodon.social. You can follow them or interact with them if you have an account anywhere in the fediverse.
If you don't, you can sign up here.
@borko I want to prove some properties about logic programs. How do I formalize them? Probably as a set of formulas...
@charlag Using the Curry-Howard correspondence.
Also, you have to work on type level.
@borko I mean
Inductive formula :=
????
.
@charlag This corresponds to a type, and you also need to define functions, obviously.
@charlag But don't listen to me too much, I might fool you. Check this tutorial, if you haven't already done so (https://coq.inria.fr/tutorial-nahas) and also I think its worth it to check Agda too.
@charlag Don’t understand the question