Stream: Miscellaneous

Topic: formal specification of Common Lisp in Coq


view this post on Zulip Lessness (Dec 25 2021 at 22:06):

How much time would it take? Human months?
How are formal specifications of programming language done? What to read to educate myself if I have such aim?
Is it possible for patient beginner to contribute/ to do that?

One thing is to go all the CompCert way and write formally verified compiler... but formalizing only the language seems easier.

view this post on Zulip Karl Palmskog (Dec 25 2021 at 22:12):

if you want a verified LISP in Coq, one approach could be to port Milawa runtime ("Jitawa") from HOL4 to Coq: https://www.kookamara.com/jared/2011-itp-jitawa.pdf

view this post on Zulip Karl Palmskog (Dec 25 2021 at 22:16):

C is a complicated language, so if you're interested in formal specs of practical programming languages, I recommend taking a look at CakeML:

For specifications of smaller languages, I recommend taking a look at Ott, which has export to Coq: github.com/ott-lang/ott


Last updated: Aug 19 2022 at 20:03 UTC