16
$\begingroup$

I started programming a Haskell-clone recently (source code).

After basic hindley-milner, problems start to arise. Implementation of data/codata statements seem to ensure my language is breaking up on every front.

At this point I seem to lack foundations for the language. System F introduces kinds, but would it be better to approach theorem provers and pick a different calculus as foundation?

Also looking for overall suggestions for this kind of a project.

$\endgroup$
2
  • 1
    $\begingroup$ Are you using "theorem provers" and "proof assistants" as synonyms? $\endgroup$ Feb 9 at 22:03
  • $\begingroup$ Yes. I meant proof assistants. $\endgroup$
    – Cheery
    Feb 10 at 10:39

2 Answers 2

13
$\begingroup$

If you are asking "can we use proof assistants to develop foundations of programming languages" then the answer is positive. Two well-known such developments are:

There are also specialized proof assistants that make it easier to develop the meta-theory of a programming language, such as Twelf, Abella and Beluga.

$\endgroup$
2
  • $\begingroup$ edits should be at least 6 characters. weird... $\endgroup$ Feb 9 at 23:33
  • $\begingroup$ Fixed, thank you. $\endgroup$ Feb 10 at 14:31
8
$\begingroup$

I'm interested in this application of theorem provers, but it's not my speciality. I can point you to Harper and Licata's paper Mechanizing Metatheory in a Logical Framework, which walks through using Twelf to prove results about a toy functional programming language.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.