Nick Benton: Publications

Bibliography (Papers, Drafts, Notes and Stuff)

2006
- N Benton, A Kennedy, M Hofmann and L Beringer. Reading, Writing and Relations: Towards Extensional Semantics for Effect Analyses. June 2006. Coq script.
- N Benton. Machine Obstructed Proof (Abstract). May 2006. ACM SIGPLAN Workshop on Mechanizing Metatheory, September 2006.
- N Benton. Abstracting Allocation: The New new Thing. To appear in Proceedings of Computer Science Logic (CSL '06) September 2006. © Springer-Verlag 2006.
- N Benton and X Leroy (eds). Proceedings of the 2005 ACM-SIGPLAN Workshop on ML (ML'05). Electronic Notes in Theoretical Computer Science (ENTCS) 148(2). March 2006. © Elsevier.
- N Benton and N Torp-Smith. Abstracting Allocation: The New new Thing. Short Presentation. In Proceedings of the Third Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE '06). January 2006. Superseded by CSL paper above.
2005
- N Benton. A Typed, Compositional Logic for a Stack-Based Abstract Machine. Proceedings of the Third Asian Symposium on Programming Languages and Systems (APLAS '05). LNCS 3780, November 2005. © Springer-Verlag 2005.
- N Benton. Embedded Interpreters. Journal of Functional Programming (JFP) 15(4):503-542. July 2005. ps. © Cambridge University Press 2005.
- N Benton. A Typed, Compositional Logic for a Stack-Based Abstract Machine. Technical Report MSR-TR-2005-84. June 2005.
- N Benton. Semantics of Program Analyses and Transformations. Lecture notes for the PAT Summer School. June 2005. (Updated with material for the last lecture.)
- N Benton and B Leperchey. Relational Reasoning in a Nominal Semantics for Storage. Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA '05). LNCS 3461, April 2005. © Springer-Verlag 2005.
- N Benton, A Kennedy, S Lindley and C Russo. Shrinking Reductions in SML.NET. Proceedings of the 16th International Workshop on Implementation and Application of Functional Languages (IFL '04). Revised Selected Papers. LNCS 3474. © Springer-Verlag 2005. A preliminary version appeared in the Draft Proceedings of IFL'04, Technical Report 0408, Institute of Computer Science and Applied Mathematics, University of Kiel.
- N Benton. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. Technical Report MSR-TR-2005-26. February 2005. This is an extended version of the POPL paper below, including the proofs.
2004
- N Benton and B Leperchey. Relational Reasoning in a Nominal Semantics for Storage (Preliminary Report). Technical Report. To appear.
- N Benton, L Cardelli and C Fournet. Modern Concurrency Abstractions for C#. ACM Transactions on Programming Languages and Systems (TOPLAS) 26(5):769-804. September 2004. © ACM 2004.
- N Benton, A Kennedy and C Russo. Adventures in Interoperability: The SML.NET Experience. Proceedings of the 6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP). August 2004. © ACM 2004.
- N Benton. A Typed Logic for Stacks and Jumps.Draft Note. March 2004. Mostly superseded by MSR-TR-2005-84 above.
- N Benton. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). January 2004. This version fixes a couple of minor errors in the proceedings version. © ACM 2004.
2003
- N Benton and M Hyland. Traced Premonoidal Categories. Theoretical Informatics and Applications 37(4):273-299, © EDP Sciences 2003.
- N Benton, P Dybjer and J Hughes. Industrial Challenges in Semantics. EU deliverable under the APPSEM II working group in the 5th Framework Programme. October 2003.
- N Benton. Jingle Bells: Solving the Santa Claus Problem in Polyphonic C#. Note. March 2003.
2002
- N Benton and M Hyland. Traced Premonoidal Categories (Extended Abstract). Proceedings of the Workshop on Fixed Points in Computer Science (FICS 2002). July 20 and 21, 2002, Copenhagen, Denmark. Superseded by JTIA paper above.
- N Benton, L Cardelli and C Fournet. Modern Concurrency Abstractions for C#. In B. Magnusson (Ed.), Proceedings of the 16th European Conference on Object-Oriented Programming (ECOOP 2002). June 10-14, 2002 University of Málaga, Spain. LNCS 2374. © Springer-Verlag 2002.
- N Benton, A Kennedy and C Russo. SML.NET User Guide. June 2002 - October 2003 (version 1.1)
- N Benton, L Cardelli and C Fournet. Modern Concurrency Abstractions for C#. Proceedings of the Ninth ACM SIGPLAN Workshop on Foundations of Object Oriented Languages (FOOL 9). Portland, Oregon, January 2002. Superseded by TOPLAS paper above.
2001
- N Benton and A Kennedy (eds). BABEL'01: Proceedings of the First ACM SIGPLAN Workshop on Multilanguage Infrastructure and Interoperability. Electronic Notes in Theoretical Computer Science 59(1), Elsevier September 2001.
- N Benton and A Kennedy. Exceptional Syntax. Journal of Functional Programming. 11(4):395-410, July 2001. © Cambridge University Press 2001.
- N Benton, A Kennedy and B McAdam. Type Inference for MLj. In Trends in Functional Programming, Volume 2. Ed. S. Gilmore. Intellect, 2001.
2000
- N Benton, J Hughes and E Moggi. Monads and Effects. APPSEM Summer School September 2000. LNCS 2395, Springer-Verlag 2002. Note: the published version is a non-trivial revision of this one. Powerpoint.
- N Benton. A Proof Sketch Of Something Which May Possibly Be A Conjecture of Oege de Moor. Note. December 2000.
1999
- N Benton and A Kennedy. Monads, Effects and Transformations. Proceedings of the 3rd International Workshop in Higher Order Operational Techniques in Semantics (HOOTS), Paris. Electronic Notes in Theoretical Computer Science 26, September 1999. © Elsevier Science B.V. 1999.
- N Benton and A Kennedy. Interlanguage Working Without Tears: Blending SML with Java. Proceedings of the 4th ACM SIGPLAN Conference on Functional Programming (ICFP), Paris, September 1999. © ACM 1999.
- N Benton. Some Shortcomings of, and Possible Improvements to, the Java Virtual Machine. Note. June 1999.
- N Benton, A Kennedy and G Russell. MLj 0.2 User Guide. February 1999.
1998
- N Benton. Pattern Transfer: Bridging the Gap between Theory and Practice. Invited talk at MathFIT Instructional Meeting on Recent Advances in Foundations for Concurrency. Imperial College, July 1998.
- N Benton, A Kennedy and G Russell. Compiling Standard ML to Java Bytecodes. Proceedings of the 3rd ACM SIGPLAN Conference on Functional Programming (ICFP), Baltimore, September 1998. © ACM 1998.
- N Benton, G Bierman and V de Paiva. Computational Types from a Logical Perspective. Journal of Functional Programming 8(2):177-193 March 1998. © Cambridge University Press 1998.
1996
- N Benton. Semantics of Programming Languages. Lecture Notes for the Computer Science Tripos part IB, Lent 1995,1996. SML code. SML code for appendix on semantic equivalence proofs as functions.
- N Benton and P Wadler. Linear Logic, Monads and the Lambda Calculus. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), Brunswick, New Jersey, July 1996. © IEEE Press 1996.
- N Benton. On the Relationship Between Formal Semantics and Static Analysis. Invited position paper. ACM Computing Surveys, June 1996. © ACM 1996.
- N Benton. A Unified Approach to Strictness Analysis and Optimising Transformations. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-388. February 1996.
1995
- N Benton. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models. Proceedings of Computer Science Logic (CSL '94), Kazimierz, Poland. Springer-Verlag LNCS 933. June 1995. [15 page version] © Springer-Verlag 1995.
- N Benton, G Bierman and V de Paiva. Computational Types from a Logical Perspective. University of Cambridge, Computer Laboratory Technical Report UCAM-CL-TR-365. May 1995. Superseded by JFP paper above.
- N Benton. Strong Normalisation for the Linear Term Calculus. Journal of Functional Programming 5(1):65-80 January 1995. © Cambridge University Press 1995.
1994
- N Benton. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-352. October 1994. [65 page version]
1993
- N Benton, G Bierman, V de Paiva and M Hyland. Linear Lambda Calculus and Categorical Models Revisited. Proceedings of Sixth Conference on Computer Science Logic (CSL). LNCS 702, 1993. © Springer-Verlag 1993.
- N Benton, G Bierman, V de Paiva and M Hyland. A Term Calculus for Intuitionistic Linear Logic. Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA). LNCS 664, 1993. © Springer-Verlag 1993.
- N Benton. Strong Normalisation for the Linear Term Calculus. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-305 July 1993. Superseded by JFP paper above.
- N Benton. Strictness Properties of Lazy Algebraic Datatypes. In Proceedings of the Third International Workshop on Static Analysis, Padova, Italy. LNCS 724, 1993. © Springer-Verlag 1993.
1992
- N Benton, G Bierman, V de Paiva and M Hyland. Term Assignment for Intuitionistic Linear Logic, Technical Report 262, University of Cambridge Computer Laboratory. August 1992.
- N Benton. Strictness Logic and Polymorphic Invariance. Proceedings of the Second International Symposium on Logical Foundations of Computer Science, Tver, Russia. LNCS 620, 1992. © Springer-Verlag 1992.
- N Benton. Strictness Analysis of Lazy Functional Programs. PhD Thesis, University of Cambridge Computer Laboratory, December 1992. Available as Technical Report 309, August 1993.

Nick Benton

Bibliography (Papers, Drafts, Notes and Stuff)

2006

2005

2004

2003

2002

2001

2000

1999

1998

1996

1995

1994

1993

1992