Bibliography (Papers, Drafts, Notes and Stuff)
2018
- N Benton, M Hofmann and V Nigam. Proof-Relevant Logical Relations for Name Generation. Logical Methods in Computer Science 14(1), 2018.
- N Benton, M Hofmann and V Nigam. Effect-dependent Transformations for Concurrent Programs. Science of Computer Programming 155:27-51, 2018.
- N Benton. Semantic Equivalence Checking for HHVM Bytecode. Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018).
2017
- K-B Hou, N Benton and R Harper. Correctness of Compiling Polymorphism to Dynamic Typing. Journal of Functional Programming. © CUP 2017.
2016
- N Benton, M Hofmann and V Nigam. Effect-Dependent Transformations for Concurrent Programs.Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016). There is also an older preprint on the arXiv and an associated draft, Computational Adequacy of Trace Semantics.
- N Benton, A Kennedy, M Hofmann and V Nigam. Counting Successes: Effects and Transformations for Non-Deterministic Programs. In A List of Successes That Can Change The World, Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. LNCS 9600. © Springer 2016.
2015
- N Benton. Categorical Monads and Computer Programming. In Impact150 - LMS 150 Year Impact Stories. London Mathematical Society, November 2015.
- N Krishnaswami, P Pradic and N Benton. Integrating Dependent and Linear Types. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). © ACM 2015.
2014
- N Benton, M Hofmann and V Nigam. Abstract Effects and Proof-Relevant Logical Relations. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014). © ACM 2014. A talk on a preliminary version of this work was presented at the 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2012). September 2012.
2013
- N Benton. The Proof Assistant as an Integrated Development Environment. Invited talk. Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS 2013). LNCS 8301. December 2013. © Springer 2013.
- A Kennedy, N Benton, J Jensen and P Dagand. Coq: The World's Best Macro Assembler? Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013). September 2013. © ACM 2013.
- N Benton, M Hofmann and V Nigam. Proof-Relevant Logical Relations for Name Generation. Proceedings of the 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013). LNCS 7941. June 2013. © Springer 2013.
- J Jensen, N Benton and A Kennedy. High-Level Separation Logic for Low-Level Code. Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013). January 2013. © ACM 2013. A related talk, Using Coq to Generate and Reason About x86 Systems Code, was presented at the 3rd Workshop on Syntax and Semantics of Low-Level Languages (LOLA 2012). And here's a poster.
2012
- N Benton and V Koutavas. A Mechanized Bisimulation for the Nu-Calculus. Preprint, September 2012. To appear in Higher Order and Symbolic Computation. Coq script.
- N Krishnaswami and N Benton. Adding Equations to System F Types. Proceedings of the 22nd European Symposium on Programming (ESOP 2012). LNCS 7211. March 2012. © Springer 2012.
- N Krishnaswami, N Benton and J Hoffmann. Higher-Order Functional Reactive Programming in Bounded Space. Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012). January 2012. © ACM 2012.
2011
- N Krishnaswami and N Benton. A Semantic Model for Graphical User Interfaces. Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP'11). September 2011. © ACM 2011.
- N Krishnaswami and N Benton. Ultrametric Semantics of Reactive Programs. Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS'11). June 2011. © IEEE 2011. Associated OCaml implementation.
- N Benton, C-K Hur, A J Kennedy and C McBride. Strongly Typed Term Representations in Coq. Journal of Automated Reasoning (2012) 49:141-159. © Springer 2011. Preprint Coq script.
- N Benton and P Johann (eds). Special Issue: Selected Papers of the Symposium "Principles of Programming Languages 2009". Logical Methods in Computer Science 2011.
2010
- A Ahmed, N Benton, L Birkedal and M Hofmann. Modelling, Controlling and Reasoning About State. Seminar Proceedings, Executive Summary and Abstracts Collection. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany 2010.
- N Benton, L Birkedal, A Kennedy and C Varming. Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages. Draft of July 2010. Coq script.
- N Benton and C-K Hur. Step-Indexing: The Good, the Bad and the Ugly. In Modelling, Controlling and Reasoning About State, Proceedings of Dagstuhl Seminar 10351, 2010. (An earlier version was presented at the Workshop on Syntax and Semantics of Low Level Languages (LOLA), July 2010.)
- N Benton and C-K Hur. Realizability and Compositional Compiler Correctness for a Polymorphic Language. Technical Report MSR-TR-2010-62. April 2010. Coq script (This version includes more theory of source-level contextual equivalence than before).
- A Kennedy and N Benton (eds). Proceedings of the 5th ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'10). January 2010. © ACM 2010
2009
- N Benton, L Beringer, M Hofmann and A Kennedy. Relational Semantics for Effect-Based Program Transformations: Higher-Order Store. Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP '09). September 2009. © ACM 2009.
- N Benton, C-K Hur and A Kennedy. Strongly Typed Term Representations in Coq. 4th ACM SIGPLAN Workshop on Mechanized Metatheory (WMM '09). September 2009. Superseded by JAR paper above.
- N Benton and C-K Hur. Biorthogonality, Step-Indexing and Compiler Correctness. Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09), August/September 2009. © ACM 2009. Coq script.
- N Benton, A Kennedy and C Varming. Some Domain Theory and Denotational Semantics in Coq. Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09).LNCS 5674, August 2009. © Springer-Verlag 2009. Coq script.
- N Benton and N Tabareau. Compiling Functional Types to Relational Specifications for Low Level Imperative Code. Proceedings of the Fourth ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '09), January 2009. © ACM 2009. Coq script.
2008
- M Ridsdale, M Jamnik, N Benton and J Berdine. Diagrammatic Reasoning in Separation Logic. Proceedings of the Fifth International Conference on the Theory and Application of Diagrams. LNCS 5223, September 2008. © Springer-Verlag 2008.
- N Benton and V Koutavas. A Mechanized Bisimulation for the Nu-Calculus. Technical Report MSR-TR-2008-129. September 2008. Superseded by Mitchfest version above.
- A Ahmed, N Benton, M Hofmann and G Morrisett. Types, Logics and Semantics for State. Executive Summary and Abstracts Collection. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2008.
- N Benton. Undoing Dynamic Typing. Proceedings of the Ninth International Symposium on Functional and Logic Programming (FLOPS '08). LNCS 4989, April 2008. © Springer-Verlag 2008.
2007
- N Benton and U Zarfaty. Formalizing and Verifying Semantic Type Soundness for a Simple Compiler. Proceedings of the Ninth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP '07), July 2007. © ACM 2007.
- N Benton, A Kennedy, M Hofmann and L Beringer. Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation. Proceedings of the Ninth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP '07), July 2007. © ACM 2007.
- N Benton and U Zarfaty. Formalizing and Verifying Semantic Type Soundness for a Simple Compiler (Preliminary Report). Technical Report MSR-TR-2007-31. March 2007.
- N Benton and P Buchlovsky. Semantics of an Effect Analysis for Exceptions. Proceedings of the Third ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '07), January 2007. © ACM 2007.
2006
- N Benton, A Kennedy, M Hofmann and L Beringer. Reading, Writing and Relations: Towards Extensional Semantics for Effect Analyses. Coq script. Proceedings of the Fourth Asian Symposium on Programming Languages and Systems (APLAS '06). LNCS 4279, November 2006. © Springer-Verlag 2006.
- N Benton. Machine Obstructed Proof (Abstract). ACM SIGPLAN Workshop on Mechanizing Metatheory, September 2006.
- N Benton. Abstracting Allocation: The New new Thing. Proceedings of Computer Science Logic (CSL '06). LNCS 4207, 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. ps. © 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. ps. 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. ps.
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. ps. © 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. ps.
- 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. ps version.
- N Benton, G Bierman and V de Paiva. Computational Types from a Logical Perspective. Journal of Functional Programming 8(2):177-193 March 1998. ps. © Cambridge University Press 1998.
1996
- N Benton. Semantics of Programming Languages. Lecture Notes for the Computer Science Tripos part IB, Lent 1995,1996. ps. 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. ps. © IEEE Press 1996.
- N Benton. On the Relationship Between Formal Semantics and Static Analysis. Invited position paper. ACM Computing Surveys, June 1996. ps. © 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. ps.
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] ps. © 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. ps. © 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] ps.
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. ps © 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. ps © 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. ps.
- 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. ps.