Stream: Miscellaneous

Topic: formal specification of Common Lisp in Coq

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.

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

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:

• https://github.com/CakeML/cakeml/tree/master/semantics (formal semantics first specified in Lem, as seen here, then exported to HOL4),
• https://cakeml.org which has a list of papers

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

Last updated: Apr 19 2024 at 00:02 UTC