|
Researcher |
|
My research interests include type systems and formal semantics for programming languages, optimizing compilation, functional programming, and high-level language interoperability. I do not believe in object-oriented programming.
Click on theme to see publications, talks, and software.
Generics for .NET ·
.NET Security ·
Units of Measure in Programming Languages ·
Functional Programming ·
Functional Programming Language Compilation ·
Effects ·
Other ·
Mechanized metatheory ·
I have a blog that presents an introduction to units-of-measure in F#.
I studied for my PhD (1992-1995) under Alan Mycroft at the University of Cambridge Computer Laboratory. My thesis topic was programming language support for checking units-of-measure in numeric types. Following that I spent a year as a postdoctoral researcher at the Laboratoire d'informatique (LIX) at Ecole Polytechnique in Paris. I then joined Persimmon IT Inc as a research scientist, and co-developed the MLj compiler for Standard ML targeting the Java Virtual Machine. Since 1999 I have been a Researcher at Microsoft Research in Cambridge, England.
Strongly Typed Term Representations in Coq (draft)
Nick Benton, Chung-Kil Hur, Andrew Kennedy and Conor McBride.
Submitted to Journal of Automated Reasoning: Special issue on Binding, Substitution and Naming.
Coq source for simply-typed language Coq source for polymorphically-typed language
Relational Semantics for Effect-Based Program Transformations: Higher-Order Store Nick Benton, Lennart Beringer, Martin Hofmann and Andrew Kennedy. In Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP '09). September 2009.
Some Domain Theory and Denotational Semantics in Coq
Nick Benton, Andrew Kennedy and Carsten Varming.
22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09). August 2009.
Talk on typed representation of syntax used in this work, presented at Semantics Lunch at University of Cambridge Computer Laboratory.
Formalizing an Extensional Semantics for Units of Measure
Andrew Kennedy. In 3rd ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM) 2008.
Slides from talk.
Compiling with Continuations, Continued
Andrew Kennedy. In Proceedings of the International Conference on Functional Programming (ICFP) 2007.
Slides from talk.
TLDI'10 (ACM SIGPLAN Workshop on Types in Language Design and Implementation) (General Chair)
CEFP'09 ((Central European Functional Programming school), presenting course on "Types for units-of-measure: theory and practice"
Types at Work: PhD and MsC School, DTU, Denmark, presenting lectures on units-of-measure
TLDI'09 (ACM SIGPLAN Workshop on Types in Language Design and Implementation) (General Chair) · OOPS'09 (Track at ACM Symposium on Applied Computing) (PC member)
ICFP'08 (ACM SIGPLAN International Conference on Functional Programming) (PC member)
TLDI'07 (ACM SIGPLAN Workshop on Types in Language Design and Implementation) (PC member) · CC 2007 (16th International Conference on Compiler Construction) (PC member)
2006 ACM SIGPLAN Workshop on ML(PC co-chair)