Pilsner swMATH ID: 20004 Software Authors: Neis, Georg; Hur, Chung-Kil; Kaiser, Jan-Oliver; McLaughlin, Craig; Dreyer, Derek; Vafeiadis, Viktor Description: Pilsner: a compositionally verified compiler for a higher-order imperative language. Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different verified compilers, it is important to develop a compositional notion of compiler correctness that is modular (preserved under linking), transitive (supports multi-pass compilation), and flexible (applicable to compilers that use different intermediate languages or employ non-standard program transformations).par In this paper, building on prior work of the second author et al. [in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12. New York, NY: Association for Computing Machinery (ACM). 59–72 (2012; Zbl 1321.68198)], we develop a novel approach to compositional compiler verification based on parametric inter-language simulations (PILS). PILS are modular: they enable compiler verification in a manner that supports separate compilation. PILS are transitive: we use them to verify Pilsner, a simple (but non-trivial) multi-pass optimizing compiler (programmed in Coq) from an ML-like source language S to an assembly-like target language T, going through a CPS-based intermediate language. Pilsner is the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Lastly, PILS are flexible: we use them to additionally verify (1) Zwickel, a direct non-optimizing compiler for S, and (2) a hand-coded self-modifying T module, proven correct w.r.t. an S-level specification. The output of Zwickel and the self-modifying T module can then be safely linked together with the output of Pilsner. All together, this has been a significant undertaking, involving several person-years of work and over 55,000 lines of Coq. Homepage: http://plv.mpi-sws.org/pils/ Keywords: compositional compiler verification; abstract types; higher-order state; parametric simulations; recursive types; transitivity Related Software: Coq; CakeML; Isabelle/HOL; CompCertTSO; CompCert; HOL; VST-Floyd; CertiCoq; Vellvm; Java Jr; Boogie; Kami; Flicker; Toolchain; Haskell; ML; GCminor; MLton; Poly/ML; gmp Cited in: 7 Documents all top 5 Cited by 40 Authors 1 Abate, Carmine 1 Amani, Sidney 1 Blanco, Roberto 1 Chen, Zilin 1 Christensen, Michael F. 1 Ciobâcă, Ştefan 1 Dreyer, Derek R. 1 Durier, Adrien 1 Fox, Anthony C. J. 1 Garg, Deepak 1 Hardekopf, Ben 1 Hriţcu, Cătălin 1 Hupel, Lars 1 Hur, Chung-Kil 1 Kaiser, Jan-Oliver 1 Klein, Gerwin 1 Kumar, Ramana 1 Lim, Japheth 1 McLaughlin, Craig A. 1 McMahan, Joseph 1 Murray, Toby 1 Myreen, Magnus O. 1 Nadathur, Gopalan 1 Nagashima, Yutaka 1 Neis, Georg 1 Nichols, Lawton 1 Nipkow, Tobias 1 Norrish, Michael 1 O’Connor, Liam 1 Owens, Scott 1 Patrignani, Marco 1 Rizkallah, Christine 1 Roesch, Jared 1 Sewell, Thomas D. 1 Sherwood, Timothy 1 Tan, Yong Kiam 1 Tanter, Éric 1 Thibault, Jérémy 1 Vafeiadis, Viktor 1 Wang, Yuting Cited in 2 Serials 1 Theoretical Computer Science 1 Journal of Functional Programming Cited in 1 Field 7 Computer science (68-XX) Citations by Year