Concrete Semantics

What Hacker News says

1. YorkshireSeasonOct 2021
   T. Nipkow, G. Klein, Concrete Semantics. http://concrete-semantics.org/

   B. C. Pierce et al, Software Foundations. https://softwarefoundations.cis.upenn.edu/

   thread
2. tom_melliorJul 2020
   Another good one is:

   * Concrete Semantics by Nipkow and Klein http://concrete-semantics.org/, which is also an introduction to the Isabelle/HOL proof assistant and formalizes all of the PL content in Isabelle

   There's also:

   * Semantics with Applications: An Appetizer by Nielson and Nielson https://www.springer.com/gp/book/9781846286919, apparently a newer edition of an older book I liked and which used to be available as a free PDF, but the link from my browser history is now broken

   Show morethread
3. hellerup89Jan 2019
   The obvious route for self-study is to go through Halmos or Axler and Rudin, plus all additional materials and study aids such as Gelbaum & Olmsted, emulating the most popular Harvard Math 55 incarnation. Another nice Math 55 incarnation covered Hubbard & Hubbard, which is a wonderful book.

   Although Math 55 is tough, if you are self-paced and have a bit of mathematical maturity I think it is doable. It's also an excellent pure math bootcamp that gives you a solid foundation to branch into any other pure or advanced math topic.

   I have gone through Halmos & Rudin myself, and it is a great experience. However, if your end goals are more geared towards pure CS, an alternative route might be much more appropriate. Very interesting and promising parts of CS, such as formal methods, and the foundations of mathematics themselves depend on abstract algebra and logic: https://ncatlab.org/nlab/show/computational+trinitarianism

   A minor problem is that beginner literature is not so polished as it is relatively young. But there are some excellent textbooks nonetheless. Some below. Other suggestions welcome:

   * http://www.cs.man.ac.uk/~pt/Practical_Foundations/

   * https://www.mta.ca/~rrosebru/setsformath/

   * https://github.com/ademinn/ttfv/blob/master/2006.%20Sorensen...

   * http://www21.in.tum.de/~nipkow/Concrete-Semantics/

   * http://adam.chlipala.net/frap/

   * https://softwarefoundations.cis.upenn.edu/

   Show morethread
4. nextosJan 2019
   Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background):

   * Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/

   * Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/

   * FRAP (Chlipala): http://adam.chlipala.net/frap/

   * Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking

   * Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100

   * Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/

   Show morethread
5. mafribeJan 2017
   The problem with verifying realistic compilers is scale. We have known how to do it in principle since forever, and verification of toy compilers is part of textbooks on verification, such as [1], see also [2]. Realistic compilers are very complicated and Leroy's verification of CompCert took several man years for one of the world's leading compiler and verification guys. The purpose of research like CompCert and CakeML is twofold:

   - Provide a verified software toolchain for programmers with a minimal trusted computing base.

   - Investigate how the cost (in a general sense) of formal verification in general and compiler verification in particular can be lowered, ideally to the point that normal programmers can routinely use formal verification.

   The advance that CakeML makes over CompCert is bootstrapping: CakeML can compile itself, while CompCert (being a C compiler written in Ocaml) can't. Simplifying a bit, bootstrapping lowers the trusted computing base.

   Maybe Leroy's [3, 4] are good starting point for learning about this field.

   [1] T. Nipkow, G. Klein, Concrete Semantics. http://www.concrete-semantics.org/

   [2] A. Chlipala, A verified compiler for an impure functional language. http://adam.chlipala.net/papers/ImpurePOPL10

   [3] X. Leroy, Verifying a compiler: Why? How? How far? http://www.cgo.org/cgo2011/Xavier_Leroy.pdf

   [4] X. Leroy, Formal verification of a realistic compiler. http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf

   Show morethread