publications: - title: "A Certifying Square Root and Division Elimination" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2015" doi: "http://dx.doi.org/10.1016/j.entcs.2015.10.012" links: doi: "http://dx.doi.org/10.1016/j.entcs.2015.10.012" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/Neron15" researchr: "https://researchr.org/publication/Neron15" cites: 0 citedby: 0 journal: "ENTCS" volume: "317" pages: "117-131" kind: "article" key: "Neron15" - title: "A Theory of Name Resolution" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" year: "2015" doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_9" abstract: "We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two-stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and languageindependent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of α-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages." links: doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_9" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/NeronTVW15" technicalreport: "https://researchr.org/publication/TUD-SERG-2015-001" researchr: "https://researchr.org/publication/NeronTVW15" cites: 0 citedby: 0 pages: "205-231" booktitle: "ESOP" kind: "inproceedings" key: "NeronTVW15" - title: "Square Root and Division Elimination in PVS" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-642-39634-2_33" links: doi: "http://dx.doi.org/10.1007/978-3-642-39634-2_33" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Neron13" researchr: "https://researchr.org/publication/Neron13" cites: 0 citedby: 0 pages: "457-462" booktitle: "itp" kind: "inproceedings" key: "Neron13" - title: "A Quest for Exactness: Program Transformation for Reliable Real Numbers. (Transformation de Programmes pour des Nombres Réels Fiables)" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2013" doi: "https://tel.archives-ouvertes.fr/pastel-00960808" links: doi: "https://tel.archives-ouvertes.fr/pastel-00960808" dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/hal/Neron13" researchr: "https://researchr.org/publication/hal-987" cites: 0 citedby: 0 school: "École Polytechnique, Palaiseau, France" kind: "phdthesis" key: "hal-987" - title: "A constraint language for static semantic analysis based on scope graphs" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" year: "2016" doi: "http://doi.acm.org/10.1145/2847538.2847543" abstract: "In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records. " links: doi: "http://doi.acm.org/10.1145/2847538.2847543" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/AntwerpenNTVW16" researchr: "https://researchr.org/publication/AntwerpenNTVW16" cites: 0 citedby: 0 pages: "49-60" booktitle: "PEPM" kind: "inproceedings" key: "AntwerpenNTVW16" - title: "A Constraint Language for Static Semantic Analysis based on Scope Graphs with Proofs" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" year: "2015" month: "November" abstract: "In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records." links: published: "https://researchr.org/publication/VanAntwerpenNTVWPEPM2016" researchr: "https://researchr.org/publication/TUD-SERG-2015-012" cites: 0 citedby: 0 institution: "Software Engineering Research Group, Delft University of Technology" number: "TUD-SERG-2015-012" kind: "techreport" key: "TUD-SERG-2015-012" - title: "Axiomatizing Analog Algorithms" author: - name: "Olivier Bournez" link: "https://researchr.org/alias/olivier-bournez" - name: "Nachum Dershowitz" link: "https://researchr.org/alias/nachum-dershowitz" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2016" doi: "http://dx.doi.org/10.1007/978-3-319-40189-8_22" links: doi: "http://dx.doi.org/10.1007/978-3-319-40189-8_22" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cie/BournezDN16" researchr: "https://researchr.org/publication/BournezDN16" cites: 0 citedby: 0 pages: "215-224" booktitle: "CiE" kind: "inproceedings" key: "BournezDN16" - title: "Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2016" doi: "http://dx.doi.org/10.4230/DARTS.2.1.10" abstract: "Our paper introduces a systematic approach to the alignment of names in the static structure of a program, and memory layout and access during its execution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection. This Coq artifact showcases how our uniform model for memory layout in dynamic semantics provides structure to type soundness proofs. The artifact contains type soundness proofs mechanized in Coq for (supersets of) all languages in the paper. The type soundness proofs rely on a language-independent framework formalizing scope graphs and frame heaps." links: doi: "http://dx.doi.org/10.4230/DARTS.2.1.10" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/darts/PoulsenNTV16" researchr: "https://researchr.org/publication/PoulsenNTV16Artifact" cites: 0 citedby: 0 journal: "darts" volume: "2" number: "1" kind: "article" key: "PoulsenNTV16Artifact" - title: "A Constraint Language for Static Semantic Analysis based on Scope Graphs with Proofs" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" year: "2015" month: "September" abstract: "In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs—such as record field access—for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records." links: "pdf": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-009.pdf" researchr: "https://researchr.org/publication/TUD-SERG-2015-009" cites: 0 citedby: 0 institution: "Software Engineering Research Group, Delft University of Technology" number: "TUD-SERG-2015-009" kind: "techreport" key: "TUD-SERG-2015-009" - title: "A Formal Proof of Square Root and Division Elimination in Embedded Programs" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2013" doi: "http://dx.doi.org/10.6092/issn.1972-5787/3887" links: doi: "http://dx.doi.org/10.6092/issn.1972-5787/3887" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfrea/Neron13" researchr: "https://researchr.org/publication/Neron13-0" cites: 0 citedby: 0 journal: "jfrea" volume: "6" number: "1" pages: "89-111" kind: "article" key: "Neron13-0" - title: "A Formal Proof of Square Root and Division Elimination in Embedded Programs" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2012" doi: "http://dx.doi.org/10.1007/978-3-642-35308-6_20" links: doi: "http://dx.doi.org/10.1007/978-3-642-35308-6_20" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Neron12" researchr: "https://researchr.org/publication/Neron12" cites: 0 citedby: 0 pages: "256-272" booktitle: "CPP" kind: "inproceedings" key: "Neron12" - title: "SpecCert: Specifying and Verifying Hardware-Based Security Enforcement" author: - name: "Thomas Letan" link: "https://researchr.org/alias/thomas-letan" - name: "Pierre Chifflier" link: "https://researchr.org/alias/pierre-chifflier" - name: "Guillaume Hiet" link: "https://researchr.org/alias/guillaume-hiet" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Benjamin Morin" link: "https://researchr.org/alias/benjamin-morin" year: "2016" doi: "http://dx.doi.org/10.1007/978-3-319-48989-6_30" links: doi: "http://dx.doi.org/10.1007/978-3-319-48989-6_30" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fm/LetanCHNM16" researchr: "https://researchr.org/publication/LetanCHNM16" cites: 0 citedby: 0 pages: "496-512" booktitle: "FM" kind: "inproceedings" key: "LetanCHNM16" - title: "Language-Independent Type-Dependent Name Resolution" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" year: "2015" month: "July" abstract: "We extend and combine two existing declarative formalisms, the scope graphs of Neron et al. and type constraint systems, to build a language-independent theory that can describe both name and type resolution for realistic languages with complex scope and typing rules. Unlike conventional static semantics presentations, our approach maintains a clear separation between scoping and typing concerns, while still be- ing able to handle language constructs, such as class field access, for which name and type resolution are necessarily intertwined. We define a constraint scheme that can express both typing and name binding constraints, and give a for- mal notion of constraint satisfiability together with a sound algorithm for finding solutions in important special cases. We describe the details of constraint generation for a model language that illustrates many of the interesting resolution issues associated with modules, classes, and records. Our constraint generator and solver have been implemented in the Spoofax Language Workbench." links: "pdf": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-006.pdf" researchr: "https://researchr.org/publication/TUD-SERG-2015-006" cites: 0 citedby: 0 institution: "Delft University of Technology, Software Engineering Research Group" number: "TUD-SERG-2015-006" address: "Delft, The Netherlands" kind: "techreport" key: "TUD-SERG-2015-006" - title: "A Language Designer's Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs" author: - name: "Eelco Visser" link: "http://eelcovisser.org" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Vlad A. Vergu" link: "http://www.linkedin.com/in/vladv" - name: "Augusto Passalaqua" link: "http://www.linkedin.com/pub/augusto-passalaqua/9/829/b29" - name: "Gabriël Konat" link: "http://nl.linkedin.com/in/gabrielkonat" year: "2014" doi: "http://doi.acm.org/10.1145/2661136.2661149" abstract: "The realization of a language design requires multiple artifacts that redundantly encode the same information. This entails significant effort for language implementors, and often results in late detection of errors in language definitions. In this paper we present a proof-of-concept language designer's workbench that supports generation of IDEs, interpreters, and verification infrastructure from a single source. This constitutes a first milestone on the way to a system that fully automates language implementation and verification. " links: doi: "http://doi.acm.org/10.1145/2661136.2661149" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/VisserWTNVPK14" "pdf": "http://dl.acm.org/ft_gateway.cfm?id=2661149&ftid=1505232&dwn=1&CFID=550125770&CFTOKEN=54358949" researchr: "https://researchr.org/publication/VisserOnward14" cites: 0 citedby: 0 pages: "95-111" booktitle: "OOPSLA" kind: "inproceedings" key: "VisserOnward14" - title: "Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2016" doi: "10.4230/LIPIcs.ECOOP.2016.20" abstract: "Semantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper, we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework for name resolution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection. " links: dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecoop/PoulsenNTV16" technicalreport: "https://researchr.org/publication/TUD-SERG-2016-010" "pdf": "http://drops.dagstuhl.de/opus/volltexte/2016/6114/pdf/LIPIcs-ECOOP-2016-20.pdf" researchr: "https://researchr.org/publication/PoulsenNTV16" cites: 0 citedby: 0 booktitle: "ECOOP" kind: "inproceedings" key: "PoulsenNTV16" - title: "A Formal Security Model of a Smart Card Web Server" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Quang Huy Nguyen" link: "https://researchr.org/alias/quang-huy-nguyen" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-27257-8_3" links: doi: "http://dx.doi.org/10.1007/978-3-642-27257-8_3" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cardis/NeronN11" researchr: "https://researchr.org/publication/NeronN11" cites: 0 citedby: 0 pages: "34-49" booktitle: "cardis" kind: "inproceedings" key: "NeronN11" - title: "DynSem: A DSL for Dynamic Semantics Specification" author: - name: "Vlad A. Vergu" link: "http://www.linkedin.com/in/vladv" - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2015" doi: "http://dx.doi.org/10.4230/LIPIcs.RTA.2015.365" abstract: "The formal semantics of a programming language and its implementation are typically separately defined, with the risk of divergence such that properties of the formal semantics are not properties of the implementation. In this paper, we present DynSem, a domain-specific language for the specification of the dynamic semantics of programming languages that aims at supporting both formal reasoning and efficient interpretation. DynSem supports the specification of the operational semantics of a language by means of statically typed conditional term reduction rules. DynSem supports concise specification of reduction rules by providing implicit build and match coercions based on reduction arrows and implicit term constructors. DynSem supports modular specification by adopting implicit propagation of semantic components from I-MSOS, which allows omitting propagation of components such as environments and stores from rules that do not affect those. DynSem supports the declaration of native operators for delegation of aspects of the semantics to an external definition or implementation. DynSem supports the definition of auxiliary meta-functions, which can be expressed using regular reduction rules and are subject to semantic component propagation. DynSem specifications are executable through automatic generation of a Java-based AST interpreter. " links: doi: "http://dx.doi.org/10.4230/LIPIcs.RTA.2015.365" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/rta/VerguNV15" "techreport": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-003.pdf" researchr: "https://researchr.org/publication/VerguNV15" cites: 0 citedby: 0 pages: "365-378" booktitle: "RTA" kind: "inproceedings" key: "VerguNV15" - title: "Elimination of Square Roots and Divisions by Partial Inlining" author: - name: "Pierre Néron" link: "https://researchr.org/profile/pierrejeanmichelneron/publications" year: "2014" doi: "http://doi.acm.org/10.1145/2643135.2643140" links: doi: "http://doi.acm.org/10.1145/2643135.2643140" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/Neron14" researchr: "https://researchr.org/publication/Neron14" cites: 0 citedby: 0 pages: "81-92" booktitle: "ppdp" kind: "inproceedings" key: "Neron14"