Research Catalog

Research publications by past and present Galois employees.

2009

Lee Pike, Geoffrey M. Brown, and Alwyn Goodloe: Experience report: roll your own real-time simulator. In progress.
Lee Pike: How to pretty-print a long formula. In progress (paper and the pretty-printer are available).
Darren Abramson and Lee Pike: When formal systems kill: computer ethics and formal methods. Submitted (journal article). Comments solicited!
Geoffrey M. Brown and Lee Pike: Automated verification and refinement for physical-layer protocols. Submitted (journal article), 2007.
Jon Rafkind, Adam Wick, Matthew Flatt, and John Regehr: Precise Garbage Collection for C. ISMM 2009.
Lee Pike, Don Stewart, and John Van Enk: Autonomous Verification and Validation (position paper). CPS Week 2009 Workshop on Mixed Criticality
Levent Erkök and John Matthews. Pragmatic Equivalence and Safety Checking in Cryptol. PLPV 2009: 73-81.

2008

Gabriele Keller, Hugh Chaffey-Millar, Manuel M. T. Chakravarty, Don Stewart, Christopher Barner-Kowollik: Specialising Simulator Generators for High-Performance Monte-Carlo Methods. PADL 2008: 116-132
Iavor Diatchki: Experience Report: Statically-Typed Server APIs.
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews: Imperative Functional Programming with Isabelle/HOL. TPHOLs 2008: 134-149
Sandip Ray, Warren A. Hunt Jr., John Matthews, J. Strother Moore: A Mechanical Analysis of Program Verification Strategies. J. Autom. Reasoning 40(4): 245-269 (2008)
Kathleen Fisher, David Walker, Kenny Qili Zhu, Peter White: From dirt to shovels: fully automatic tool generation from ad hoc data. POPL 2008: 421-434
Lee Pike: High-Confidence Bus Architectures: The Backbone of Automotive Cyber-Physical Systems (position paper). National Workshop on High-Confidence Automotive Cyber-Physical Systems, 2008.
Johan Nordlander, Magnus Carlsson, Andy Gill: Unrestricted pure call-by-value recursion. ML 2008: 23-34.
Duncan Coutts, Isaac Potoczny-Jones and Don Stewart: Haskell: Batteries Included. HW 2008.
Levent Erkök and John Matthews. Using Yices as an Automated solver in Isabelle/HOL. AFM 2008: 3-13.

2007

Aaron Tomb, Guillaume P. Brat, Willem Visser: Variably Interprocedural Program Analysis for Runtime Error Detection. ISSTA 2007: 97-107.
David Herman, Aaron Tomb, and Cormac Flanagan: Space-Efficient Gradual Typing (2007). In Trends in Functional Programming, April 2007.
Duncan Coutts, Don Stewart, Roman Leshchinskiy: Rewriting Haskell Strings. PADL 2007: 50-64
Duncan Coutts, Roman Leshchinskiy, Don Stewart: Stream fusion: from lists to streams to nothing at all. ICFP 2007: 315-326
Don Stewart, Spencer Sjanssen: Xmonad. Haskell 2007: 119
Hugh Chaffey-Millar, Don Stewart, Manuel M. T. Chakravarty, Gabriele Keller, and Christopher Barner-Kowollik: A Parallelised High Performance Monte Carlo Simulation Approach for Complex Polymerisation Kinetics. Macromolecular Theory and Simulation 16(6), pp 575-592, 2007
Iavor Diatchki: High-Level Abstractions for Low-Level Programming.
Joe Hurd: Proof Pearl: The Termination Analysis of Terminator. TPHOLs 2007: 151-156
Lee Pike: Model checking for the practical verificationist: a user’s perspective on SAL. In Automated Formal Methods (AFM07), 2007.
Lee Pike: Modeling time-triggered protocols and verifying their real-time schedules. In Formal Methods in Computer Aided Design (FMCAD 2007), 2007.
Geoffrey Brown and Lee Pike: Temporal refinement using SMT and model checking with an application to physical-layer protocols. In Fifth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’2007), 2007.
Simon Marlow and José Iborra and Bernard Pope and Andy Gill: A lightweight interactive debugger for Haskell, Proceedings of the 2007 ACM SIGPLAN Workshop on Haskell, September 2007
Andy Gill and Colin Runciman: Haskell Program Coverage, Proceedings of the 2007 ACM SIGPLAN Workshop on Haskell, September 2007
Rebekah Leslie, Levent Erkök and Flemming Andersen. Formalizing Information Flow in a Haskell Hypervisor. MIKES 2007.

2006

Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan: Sage: Hybrid Checking for Flexible Specifications. In Workshop on Scheme and Functional Programming, September 2006.
Cormac Flanagan, Stephen N. Freund, and Aaron Tomb: Hybrid Types, Invariants, and Refinements for Imperative Objects.
Iavor Diatchki, Mark P. Jones: Strongly typed memory areas programming systems-level data structures in a functional language. Haskell 2006: 72-83
Isaac Jones: Haskell’ status report. Haskell 2006: 122
Lee Pike, Mark Shields, John Matthews: A verifying core for a cryptographic language compiler. ACL2 2006: 1-10
John Matthews, J. Strother Moore, Sandip Ray, Daron Vroon: Verification Condition Generation Via Theorem Proving. LPAR 2006: 362-376
Lee Pike, Paul Miner, and Wilfredo Torres-Pomales: Diagnosing a failed proof in fault-tolerance: a disproving challenge problem. In Disproving ’06 (Participants’ proceedings), 2006
Lee Pike: A note on inconsistent axioms in Rushby’s "Systematic formal verification for fault-tolerant time-triggered algorithms". In IEEE Transactions on Software Engineering, 32(5): 347-348, 2006
Geoffrey Brown and Lee Pike: "Easy" parameterized verification of cross clock domain protocols. In Designing Correct Circuits (DCC’06) (Participants’ Proceedings), 2006.
Geoffrey Brown and Lee Pike: Easy parameterized verification of biphase and 8N1 protocols. In 12th International Conference on Tools and Algorithms for the Construction and Analysis of Algorithms (TACAS’06), volume 3920 of LNCS, pages 58--72, 2006. Springer.
Lee Pike: Formal Verification of Time-Triggered Systems. Ph.D dissertation, Indiana University, 2006.
Adam Wick: Magpie: Precise Garbage Collection For C. PhD Dissertation, University of Utah, 2006.
Andy Gill: Introducing the Haskell Equational Reasoning Assistant, Proceedings of the 2006 ACM SIGPLAN Workshop on Haskell, 2006

2005

Aaron Tomb and Cormac Flanagan: Automatic Type Inference via Partial Evaluation. In Principles and Practice of Declarative Programming, July 2005.
Don Stewart, Manuel M. T. Chakravarty: Dynamic applications from the ground up. Haskell 2005: 27-38
Iavor Diatchki, Mark P. Jones, Rebekah Leslie: High-level views on low-level representations. ICFP 2005: 168-179
Isaac Jones: Halfs: a haskell filesystem. Haskell 2005: 116
Joe Hurd, Thomas F. Melham: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005,Proceedings Springer 2005
Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang: Functional Correctness Proofs of Encryption Algorithms. LPAR 2005: 519-533
Joe Hurd, Annabelle McIver, Carroll Morgan: Probabilistic Guarded Commands Mechanized in HOL. Electr. Notes Theor. Comput. Sci. 112: 95-111 (2005)
Brian Huffman, John Matthews, Peter White: Axiomatic Constructor Classes in Isabelle/HOLCF. TPHOLs 2005: 147-16
Lee Pike and Steven D. Johnson: The formal verification of a reintegration protocol. In EMSOFT ’05: Proceedings of the 5th ACM international conference on Embedded software, pages 286--289, 2005. ACM Press.
Lee Pike: Real-time system verification by k-induction. NASA Technical Memorandum TM-2005-213751, 2005.

2004

Andre Pang, Don Stewart, Sean Seefried, and Manuel M. T. Chakravarty: Plugging Haskell In. In Proceedings of the ACM SIGPLAN Workshop on Haskell, pages 10-21. ACM Press, 2004
Sava Krstic, John Matthews: Semantics of the reFL^ect language. PPDP 2004: 32-42
Lee Pike, Paul Miner, and Wilfredo Torres-Pomales: Model checking failed conjectures in theorem proving: a case study. NASA Technical Memorandum TM-2004-213278, 2004
Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser: Abstractions for fault-tolerant distributed system verification. In Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of LNCS, pages 257--270. 2004. Springer.
Gerard Allwein, Hilmi Demir, and Lee Pike: Logics for classes of boolean monoids. In Journal of Logic, Language and Information, 13(3): 241--266, 2004
Paul Miner, Alfons Geser, Lee Pike, and Jeffery Maddalon: A unified fault-tolerance protocol. In Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of LNCS, pages 167--182, 2004. Springer.
Adam Wick, Matthew Flatt: Memory Accounting Without Partitions. ISMM 2004.
Levent Erkök: Formal verification of Controller transactions using Computation Tree Logic, Intel DTTC 2004.

2003

Andrew Moran, David Sands, Magnus Carlsson: Erratic Fudgets: a semantic theory for an embedded coordination language. Sci. Comput. Program. 46 (1-2): 99-135 (2003)
Avik Sinha, Carol Smidts, Andrew Moran: Enhanced Testing of Domain Specific Applications by Automatic Extraction of Axioms from Functional Specifications. ISSRE 2003: 181-190
Michael J. C. Gordon, Joe Hurd, Konrad Slind: Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. CHARME 2003: 200-215
Konrad Slind, Joe Hurd: Applications of Polytypism in Theorem Proving. TPHOLs 2003: 103-119
Joe Hurd: Verification of the Miller-Rabin probabilistic primality test. J. Log. Algebr. Program. 56(1-2): 3-21 (2003)
Sava Krstic, John Matthews: Inductive Invariants for Nested Recursion. TPHOLs 2003: 253-269
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu: Checking Cache-Coherence Protocols with TLA^ . Formal Methods in System Design 22(2): 125-131 (2003)
Magnus Carlsson, Johan Nordlander, Dick Kieburtz: The Semantic Layers of Timber. APLAS 2003: 339-356
Williams Harrison, Mark Tullsen, James Hook: Domain Separation by Construction (2003),
Brian Ensink, Joel Stanley, Vikram S. Adve: Program Control Language: a programming language for adaptive distributed applications. J. Parallel Distrib. Comput. 63(11): 1082-1104 (2003)

2002

Levent Erkök, John Launchbury, Andrew Moran: Semantics of value recursion for Monadic Input/Output. ITA 36(2): 155-180 (2002)
Levent Erkök, John Launchbury: A Recursive do for Haskell. Proc. of 2002 ACM SIGPLAN Workshop on Haskell, Haskell’02 (Pittsburgh, PA, USA, 3 Oct. 2002), pp. 29-37, ACM Press, 2002.
David Sands, Jurgen Gustavsson, Andrew Moran: Lambda Calculi and Linear Speedups. The Essence of Computation 2002: 60-84
Iavor Diatchki: A Formal Specification of the Haskell 98 Module System.
Joe Hurd: An LCF-Style Interface between HOL and First-Order Logic. CADE 2002: 134-138
Joe Hurd: A Formal Approach to Probabilistic Termination. TPHOLs 2002: 20-245
Leslie Lamport, John Matthews, Mark R. Tuttle, Yuan Yu: Specifying and verifying systems with TLA . ACM SIGOPS European Workshop 2002: 45-48
Sava Krstic, John Matthews: Verifying BDD Algorithms through Monadic Interpretation. VMCAI 2002: 182-195
Magnus Carlsson: Monads for incremental computing. ICFP 2002: 26-35
Johan Nordlander, Mark P. Jones, Magnus Carlsson, Richard B. Kieburtz, Andrew P. Black: Reactive Objects. Symposium on Object-Oriented Real-Time Distributed Computing 2002: 155-158
Mark Tullsen: PATH, A Program Transformation System for Haskell.
Adam Wick, Matthew Flatt, Wilson Hsieh: Reachability-based Memory Accounting. 2002 Scheme Workshop.
Levent Erkök: Value Recursion in Monadic Computations. PhD Dissertation, Oregon Graduate Institute School of Science Engineering, OHSU. October 2002.

2001

Simon Marlow, Simon L. Peyton Jones, Andrew Moran, John H. Reppy: Asynchronous Exceptions in Haskell. PLDI 2001: 274-285
Andrew Moran, Jim Teisher, Andrew Gill, Emir Pasalic, John Veneruso: Automated translation of legacy code for ATE. ITC 2001: 148-156
Dylan McNamee, Jonathan Walpole, Calton Pu, Crispin Cowan, Charles Krasic Ashvin Goel, Perry Wagle, Charles Consel, Gilles Muller, Renaud Marlet: Specialization tools and techniques for systematic optimization of system software. ACM Trans. Comput. Syst. 19(2): 217-251 (2001)
Joe Hurd: Predicate Subtyping with Predicate Sets. TPHOLs 2001: 265-280
Joe Hurd: Congruence Classes with Logic Variables. Logic Journal of the IGPL 9(1): (2001)
Sava Krstic, John Launchbury, Dusko Pavlovic: Categories of Processes Enriched in Final Coalgebras. FoSSaCS 2001: 303-317
Thomas Nordin, Andrew P. Tolmach: Modular lazy search for Constraint Satisfaction Problems. J. Funct. Program. 11(5): 557-587 (2001)
Levent Erkök, John Launchbury, Andrew Moran: Semantics of fixIO. Workshop on Fixed points in Computer Science Workshop, FICS’01. Firenze, Italy. September, 2001.

2000

David C. Steere, Antonio M. Baptista, Dylan McNamee, Calton Pu, Jonathan Walpole: Research challenges in environmental observation and forecasting systems. MOBICOM 2000: 292-299
Jeffrey Lewis, John Launchbury, Erik Meijer, Mark Shields: Implicit Parameters: Dynamic Scoping with Static Types. POPL 2000: 108-118
Levent Erkok, John Launchbury: Recursive monadic bindings. ICFP 2000: 174-185
Mark Tullsen: The Zip Calculus. MPC 2000: 28-44
Mark Tullsen: First Class Patterns. PADL 2000: 1-15
Andy Gill: Debugging Haskell by observing intermediate data structures. Proceedings of the 2000 ACM SIGPLAN Workshop on Haskell, Technical report of the University of Nottingham, 2000
Erik Meijer, Sigbjorn Finne: Lambada, Haskell as a Better Java. Electr. Notes Theor. Comput. Sci. 41(1): (2000)
Conal Elliott, Sigbjorn Finne, Oege de Moor: Compiling Embedded Languages. SAIG 2000: 9-27

1999

Andrew Moran, Soren B. Lassen, Simon L. Peyton Jones: Imprecise Exceptions, Co-Inductively. Electr. Notes Theor. Comput. Sci. 26: (1999)
Andrew Moran, David Sands: Improvement in a Lazy Context: An Operational Theory for Call-by-Need. POPL 1999: 43-56
Soren B. Lassen, Andrew Moran: Unique Fixed Point Induction for McCarthy’s Amb. MFCS 1999: 198-208
Andrew Moran, David Sands, Magnus Carlsson: Erratic Fudgets: A Semantic Theory for an Embedded Coordination Language. COORDINATION 1999: 85-102
David C. Steere, Ashvin Goel, Joshua Gruenberg, Dylan McNamee, Calton Pu, Jonathan Walpole: A Feedback-driven Proportion Allocator for Real-Rate Scheduling. OSDI 1999: 145-158
Joe Hurd: Integrating Gandalf and HOL. TPHOLs 1999: 311-322
John Launchbury, Jeffrey Lewis, Byron Cook: On Embedding a Microarchitectural Design Language within Haskell. ICFP 1999: 60-69
Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz: Formal Verification of Explicitly Parallel Microprocessors. CHARME 1999: 23-36
John Matthews, John Launchbury: Elementary Microarchitecture Algebra. CAV 1999: 288-300
John Matthews: Recursive Function Definition over Coinductive Types. TPHOLs 1999: 73-90
Mark Tullsen, Paul Hudak: Shifting Expression Procedures into Reverse. PEPM 1999: 95-104
Sigbjorn Finne, Daan Leijen, Erik Meijer, Simon L. Peyton Jones: Calling Hell From Heaven and Heaven From Hell. ICFP 1999: 114-125

1998

Simon L. Peyton Jones, Mark Shields, John Launchbury, Andrew P. Tolmach: Bridging the Gulf: A Common Intermediate Language for ML and Haskell. POPL 1998: 49-61
John Matthews, Byron Cook, John Launchbury: Microprocessor Specification in Hawk. ICCL 1998: 90-101
Fast mergeable integer maps, Chris Okasaki and Andy Gill, ACM SIGPLAN Workshop on ML, September 1998.
Sigbjorn Finne, Daan Leijen, Erik Meijer, Simon L. Peyton Jones: H/Direct: A Binary Foreign Language Interface for Haskell. ICFP 1998: 153-162

1997

K. Al-Saqabi, Robert M. Prouty, Dylan McNamee, Steve W. Otto, Jonathan Walpole: Dynamic Load Distribution with MPVM. PDPTA 1997: 392-401
Jef Bell, Francoise Bellegarde, James Hook: Type-Driven Defunctionalization. ICFP 1997: 25-37
Byron Cook, John Launchbury: Disposable Memo Functions (Extended Abstract). ICFP 1997: 310
John Launchbury, Amr Sabry: Monadic State: Axiomatization and Type Safety. ICFP 1997: 227-238
Simon L. Peyton Jones, Thomas Nordin, Dino Oliva: C-: A Portable Assembly Language. Implementation of Functional Languages 1997: 1-19

1996

Richard B. Kieburtz, Laura McKinney, Jef Bell, James Hook, Alex Kotov, Jeffrey Lewis, Dino Oliva, Tim Sheard, Ira Smith, Lisa Walton: A Software Engineering Experiment in Software Component Generation. ICSE 1996 : 542-552
John Launchbury, Gebreselassie Baraki: Representing Demand by Partial Projections. J. Funct. Program. 6(4): 563-585 (1996
John Launchbury, Ross Paterson: Parametricity and Unboxing with Unpointed Types. ESOP 1996: 204-218
John Launchbury, Erik Meijer, Tim Sheard: Advanced Functional Programming, Second International School, Olympia, WA, USA, August 26-30, 1996, Tutorial Text Springer 1996
John Matthews, Charles U. Martel: Parallel Algorithms Using Unreliable Broadcasts. IPPS 1996: 692-696
Mark Tullsen: Compiling Haskell to Java
Andrew Gill: Cheap deforestation for non-strict functional languages. The University of Glasgow, January 1996
Simon L. Peyton Jones, Andrew Gordon, Sigbjorn Finne: Concurrent Haskell. POPL 1996: 295-308
Sigbjorn Finne, Simon L. Peyton Jones: Composing the User Interface with Haggis. Advanced Functional Programming 1996: 1-37

1995

John Hughes, Andrew Moran: Making Choices Lazily. FPCA 1995: 108-119
Brian N. Bershad, Craig Chambers, Susan J. Eggers, Chris Maeda, Dylan McNamee, Przemyslaw Pardyak, Stefan Savage, Emin GÃ¼n Sirer: SPIN - An Extensible Microkernel for Application-specific Operating System Services. Operating Systems Review 29(1): 74-77 (1995)
Richard B. Kieburtz, Francoise Bellegarde, Jef Bell, James Hook, Jeffrey Lewis, Dino Oliva, Tim Sheard, Lisa Walton, Tong Zhou: Calculating Software Generators from Solution Specifications. TAPSOFT 1995: 546-560
Richard B. Kieburtz, Jeffrey Lewis: Programming with Algebras. Advanced Functional Programming 1995: 267-307
John Launchbury, Simon L. Peyton Jones: State in Haskell. Lisp and Symbolic Computation 8(4): 293-341 (1995)
David J. King, John Launchbury: Structuring Depth-First Search Algorithms in Haskell. POPL 1995: 344-354
John Launchbury, Tim Sheard: Warm Fusion: Deriving Build-Cata’s from Recursive Definitions. FPCA 1995: 314-323
John Launchbury: Graph Algorithms with a Functional Flavous. Advanced Functional Programming 1995: 308-331
Thomas Hallgren, Magnus Carlsson: Programming with Fudgets. Advanced Functional Programming 1995: 137-182
Andy Gill: The technology behind a graphical user interface for an equational reasoning assistant. Proceedings of the 1995 Glasgow Workshop on Functional Programming, Electronic Workshops in Computing, Ullapool, Scotland, 1995.
Sigbjorn Finne, Simon L. Peyton Jones: Picture: A Simple Structured Graphics Model. Functional Programming 1995: 4
Sigbjorn Finne, Simon L. Peyton Jones: Composing Haggis. Eurographics Workshop on Programming Paradigms in Graphics 1995: 85-101

1994

Brian N. Bershad, Craig Chambers, Susan J. Eggers, Chris Maeda, Dylan McNamee, Przemyslaw Pardyak, Stefan Savage, Emin GÃ¼n Sirer: SPIN - An Extensible Microkernel for Application-specific Operating System Services. ACM SIGOPS European Workshop 1994: 68-71
Jef Bell, Francoise Bellegarde, James Hook, Richard B. Kieburtz, Alex Kotov, Jeffrey Lewis, Laura McKinney, Dino Oliva, Tim Sheard, L. Tong, Lisa Walton, Tong Zhou: Software design for reliability and reuse: a proof-of-concept demonstration. TRI-Ada 1994: 396-404
John Hughes, John Launchbury: Reversing Abstract Interpretations. Sci. Comput. Program. 22(3): 307-326 (1994)
John Launchbury, Simon L. Peyton Jones: Lazy Functional State Threads. PLDI 1994: 24-35
John Launchbury, Simon L. Peyton Jones: Lazy Funtional State Threads: An Abstract. ICLP 1994: 3-5
Andrew Gill and Simon Peyton Jones: Cheap Deforestation in Practice: An Optimizer for Haskell. IFIP Congress (1), 1994.

1993

Paul A. Bailes, Ming Gong, Andrew Moran: Why Functional Languages Really Need Parallelism. ICCI 1993: 423-427
Gregor Kiczales, John Lamping, Chris Maeda, David Keppel, Dylan McNamee: The Need for Customizable Operating Systems. Workshop on Workstation Operating Systems 1993: 165-169
Paul Barton-Davis, Dylan McNamee, Raj Vaswani, Edward D. Lazowska: Adding Scheduler Activations to Mach 3.0. USENIX MACH Symposium 1993: 119-136
Simon L. Peyton Jones, John Hughes, John Launchbury: How to Give a Good Research Talk. SIGPLAN Notices 28(11): 9-12 (1993)
John Launchbury: A Natural Semantics for Lazy Evaluation. POPL 1993: 144-154
Andrew Gill, John Launchbury, Simon L. Peyton Jones: A Short Cut to Deforestation. FPCA 1993: 223-232
John Launchbury, Patrick M. Sansom: Functional Programming, Glasgow 1992, Proceedings of the 1992 Glasgow Workshop on Functional Programming, Ayr, Scotland, 6-8 July 1992 Springer 1993
Sigbjorn Finne, Geoffrey L. Burn: Assessing the Evaluation Transformer Model of Reduction on the Spineless G-machine. FPCA 1993: 331-340

1992

John Hughes, Andrew Moran: A Semantics for Locally Bottom-Avoiding Choice. Functional Programming 1992: 102-112
John Hughes, John Launchbury: Projections for Polymorphic First-Order Strictness Analysis. Mathematical Structures in Computer Science 2(3): 301-326 (1992)
John Hughes, John Launchbury: Relational Reversal of Abstract Interpretation. J. Log. Comput. 2(4): 465-482 (1992)
John Launchbury, Andy Gill, John Hughes, Simon Marlow, Simon L. Peyton Jones, Philip Wadler: Avoiding Unnecessary Updates. Functional Programming 1992: 144-153
John Hughes, John Launchbury: Reversing Abstract Interpretations. ESOP 1992 : 269-286

1991

John Launchbury: Strictness and Binding-Time Analyses: Two for the Price of One. PLDI 1991: 80-91
Ryszard Kubiak, John Hughes, John Launchbury: Implementing Projection-based Strictness Analysis. Functional Programming 1991: 207-224
Simon L. Peyton Jones, John Launchbury: Unboxed Values as First Class Citizens in a Non-Strict Functional Language. FPCA 1991: 636-666
John Launchbury: A Strongly-Typed Self-Applicable Partial Evaluator. FPCA 1991: 145-164
Andrew Gill: A Novel Approach Towards Peephole Optimisations.Proceedings of the 1991 Glasgow Workshop on Functional Programming, August 1991

1990

Dylan McNamee, Katherine Armstrong: Extending the Mach External Pager Interface to Accomodate User-Level Page Replacement Policies. USENIX MACH Symposium 1990: 17-30
John Launchbury: Strictness Analysis Aids Inductive Proofs. Inf. Process. Lett. 35(3): 155-159 (1990)

1989

R. Frost, John Launchbury: Constructing Natural Language Interpreters in a Lazy Functional Language. Comput. J. 32(2): 108-121 (1989)
John Launchbury: Dependent Sums Express Separation of Binding Times. Functional Programming 1989: 238-253

1987

Guy Argo, John Hughes, Philip W. Trinder, Jon Fairbairn, John Launchbury: Implementing Functional Databases. DBPL 1987: 165-176