Research Catalog

Research publications by past and present Galois employees.

2009

Levent Erkök, Magnus Carlsson, and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol. In Formal Methods in Computer Aided Verification Conference, FMCAD’09, Austin, TX, November 2009, IEEE.
Levent Erkök and John Matthews. High assurance programming in Cryptol. In CSIIRW’09: Proceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research, Oak Ridge, TN, April 2009, ACM.
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 Erkök, 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, Sigbjørn Finne: Lambada, Haskell as a Better Java. Electr. Notes Theor. Comput. Sci. 41(1): (2000)
Conal Elliott, Sigbjørn Finne, Oege de Moor: Compiling Embedded Languages. SAIG 2000: 9-27

1999

Andrew Moran, Søren 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
Søren 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
Sigbjørn 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
Andrew Moran: Call-by-name, Call-by-need, and McCarthy’s Amb. Ph.D. thesis, 1998. Dept. of Computing Science, Chalmers University of Technology and University of Gothenburg, Sweden.
Chris Okasaki, Andy Gill: Fast mergeable integer maps. ACM SIGPLAN Workshop on ML, September 1998.
Sigbjørn 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, Sigbjørn Finne: Concurrent Haskell. POPL 1996: 295-308
Sigbjørn 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.
Sigbjørn Finne, Simon L. Peyton Jones: Picture: A Simple Structured Graphics Model. Functional Programming 1995: 4
Sigbjørn Finne, Simon L. Peyton Jones: Composing Haggis. Eurographics Workshop on Programming Paradigms in Graphics 1995: 85-101
Paul A. Pritchard, Andrew Moran, Anthony Thyssen: Twenty-two primes in arithmetic progression. July 1995, Mathematics of Computation, Vol. 64, Issue 211.

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
Sigbjørn 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