Andrew Kennedy

Researcher

Programming Principles and Tools Group
Microsoft Research Cambridge
7 J J Thomson Avenue Cambridge CB3 0FB, UK



Email: akenn@microsoft.com
Phone: +44 (1223) 479805 (Work)
Fax: +44 (1223) 479999

Research Interests

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 ·

Blog

I have a blog that presents an introduction to units-of-measure in F#.

Biography

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.

Recent publications

Abstraction and Invariance for Algebraically-Indexed Types
Robert Atkey, Patricia Johann and Andrew Kennedy. To appear in proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2013). Janary 2013.

High-Level Separation Logic for Low-Level Code
Nick Benton, Jonas Jensen and Andrew Kennedy. To appear in proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2013). Janary 2013.

Using Coq to Generate and Reason About x86 Systems Code
Nick Benton, Jonas Jensen and Andrew Kennedy. Workshop on Syntax and Semantics of Low-Level Languages (LOLA 2012). June 2012.

Every Bit Counts: The binary representation of typed data and programs
Andrew Kennedy and Dimitrios Vytiniotis. Journal of Functional Programming, 2012, to appear.

Types for Units-of-Measure: Theory and Practice
Andrew Kennedy. Lecture notes for CEFP'09, Revised July 2010, to appear in LNCS.

Functional Pearl: Every Bit Counts
Dimitrios Vytiniotis and Andrew Kennedy. In Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP), 2010.

Strongly Typed Term Representations in Coq
Nick Benton, Chung-Kil Hur, Andrew Kennedy and Conor McBride. Journal of Automated Reasoning: Special issue on Binding, Substitution and Naming, March 2011.

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.

Coq source

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.


Professional Activities

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)