publications: - title: "Practical Tactics for Separation Logic" author: - name: "Andrew McCreight" link: "http://web.cecs.pdx.edu/~mccreigh/" year: "2009" doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_24" links: doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_24" tags: - "logic" researchr: "https://researchr.org/publication/McCreight09" cites: 0 citedby: 0 pages: "343-358" booktitle: "Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings" editor: - name: "Stefan Berghofer" link: "https://researchr.org/alias/stefan-berghofer" - name: "Tobias Nipkow" link: "https://researchr.org/alias/tobias-nipkow" - name: "Christian Urban" link: "https://researchr.org/alias/christian-urban" - name: "Makarius Wenzel" link: "https://researchr.org/alias/makarius-wenzel" volume: "5674" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-03358-2" kind: "inproceedings" key: "McCreight09" - title: "A Meta Linear Logical Framework" author: - name: "Andrew McCreight" link: "http://web.cecs.pdx.edu/~mccreigh/" - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" year: "2008" doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.016" links: doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.016" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/McCreightS08" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "199" pages: "129-147" kind: "article" key: "McCreightS08" - title: "A general framework for certifying garbage collectors and their mutators" author: - name: "Andrew McCreight" link: "http://web.cecs.pdx.edu/~mccreigh/" - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" - name: "Chunxiao Lin" link: "https://researchr.org/alias/chunxiao-lin" - name: "Long Li" link: "https://researchr.org/alias/long-li" year: "2007" doi: "http://doi.acm.org/10.1145/1250734.1250788" links: doi: "http://doi.acm.org/10.1145/1250734.1250788" researchr: "https://researchr.org/publication/McCreightSLL07" cites: 0 citedby: 0 pages: "468-479" booktitle: "Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007" editor: - name: "Jeanne Ferrante" link: "https://researchr.org/alias/jeanne-ferrante" - name: "Kathryn S. McKinley" link: "https://researchr.org/alias/kathryn-s.-mckinley" publisher: "ACM" isbn: "978-1-59593-633-2" kind: "inproceedings" key: "McCreightSLL07" - title: "A verifiable SSA program representation for aggressive compiler optimization" author: - name: "Vijay Menon" link: "https://researchr.org/alias/vijay-menon" - name: "Neal Glew" link: "https://researchr.org/alias/neal-glew" - name: "Brian R. Murphy" link: "https://researchr.org/alias/brian-r.-murphy" - name: "Andrew McCreight" link: "http://web.cecs.pdx.edu/~mccreigh/" - name: "Tatiana Shpeisman" link: "https://researchr.org/alias/tatiana-shpeisman" - name: "Ali-Reza Adl-Tabatabai" link: "https://researchr.org/alias/ali-reza-adl-tabatabai" - name: "Leaf Petersen" link: "https://researchr.org/alias/leaf-petersen" year: "2006" doi: "http://doi.acm.org/10.1145/1111037.1111072" links: doi: "http://doi.acm.org/10.1145/1111037.1111072" tags: - "optimization" - "compiler" - "program optimization" researchr: "https://researchr.org/publication/MenonGMMSAP06" cites: 0 citedby: 0 pages: "397-408" booktitle: "Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006" editor: - name: "J. Gregory Morrisett" link: "https://researchr.org/alias/j.-gregory-morrisett" - name: "Simon L. Peyton Jones" link: "http://research.microsoft.com/en-us/people/simonpj/" publisher: "ACM" isbn: "1-59593-027-2" kind: "inproceedings" key: "MenonGMMSAP06" - title: "A certified framework for compiling and executing garbage-collected languages" author: - name: "Andrew McCreight" link: "http://web.cecs.pdx.edu/~mccreigh/" - name: "Tim Chevalier" link: "https://researchr.org/alias/tim-chevalier" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" year: "2010" doi: "http://doi.acm.org/10.1145/1863543.1863584" abstract: "We describe the design, implementation, and use of a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor, that includes primitives for allocating memory in a garbage-collected heap and for specifying GC roots; (ii) a precise, low-level specification for a Cminor library for garbage collection; and (iii) a proven semantics-preserving translation from GCminor to Cminor plus the GC library. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the Glasgow Haskell Compiler's Core intermediate language to GCminor. To support a simple but useful memory safety argument for this compiler, the front end uses a novel combination of type preservation and runtime checks, which is of independent interest. " links: doi: "http://doi.acm.org/10.1145/1863543.1863584" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/McCreightCT10" tags: - "programming languages" - "semantics" - "translation" - "application framework" - "program verification" - "language design" - "Haskell" - "source-to-source" - "type checking" - "compiler" - "design" - "open-source" researchr: "https://researchr.org/publication/McCreightCT10" cites: 37 citedby: 0 pages: "273-284" booktitle: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" kind: "inproceedings" key: "McCreightCT10" - title: "Foundational Typed Assembly Language with Certified Garbage Collection" author: - name: "Chunxiao Lin" link: "https://researchr.org/alias/chunxiao-lin" - name: "Andrew McCreight" link: "http://web.cecs.pdx.edu/~mccreigh/" - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" - name: "Yiyun Chen" link: "https://researchr.org/alias/yiyun-chen" - name: "Yu Guo" link: "https://researchr.org/alias/yu-guo" year: "2007" doi: "http://doi.ieeecomputersociety.org/10.1109/TASE.2007.28" links: doi: "http://doi.ieeecomputersociety.org/10.1109/TASE.2007.28" researchr: "https://researchr.org/publication/LinMSCG07" cites: 0 citedby: 0 pages: "326-338" booktitle: "First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007, June 5-8, 2007, Shanghai, China" publisher: "IEEE Computer Society" kind: "inproceedings" key: "LinMSCG07"