Bibliography (Papers, Drafts, Notes and Stuff)
2009
-
N Benton, C-K Hur, A Kennedy and C McBride. Strongly Typed Term Representations in Coq. Draft of November 2009. Coq script.
-
N Benton and C-K Hur. Compositional Compiler Correctness with Quantified Types. Draft of October 2009. Coq script.
- 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 Informal ACM SIGPLAN Workshop on Mechanized Metatheory (WMM '09). September 2009.
- 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
-
N Benton and V Koutavas. A Mechanized Bisimulation for the Nu-Calculus. Coq script.
Technical Report MSR-TR-2008-129. September 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.
-
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
2006
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
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
1999
1998
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
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.