|
1570 Bridgeview Drive |
kevin.watkins@gmail.com |
Extensive programming experience; languages include C++, Java, Perl, Haskell, ML, Scheme, Mathematica. Other experience: TCP/IP/sockets, threads/concurrency, assembly, Unix, Linux kernel, Windows, cygwin, CVS/svn/darcs, Eclipse, XML, SQL, OpenGL. Research background includes published work in language design and formal analysis of software.
Ph.D. candidate in Computer Science, Carnegie Mellon University
M.S. in Computer Science, Carnegie Mellon University, 2006
B.S. in Mathematics and Computer Science, Harvey Mudd College, 1998
SeLF (Distributed System Security via Logical Frameworks) Project, 2004-present
Contributions to a research program on the application of logical frameworks based on linear logic to the specification of security and access-control policies. My contributions have included working out the theory of the CLF framework on which the project was based; contributing to the design and theory of the LolliMon logic programming language; and presenting the results of my part of the work at the Office of Naval Research, Washington, D.C.
Concurrent Logical Framework (CLF), 2001-present
Has been the primary contributor to the development of CLF, a logical framework based on linear logic and aimed at specifying and reasoning about concurrent computation. This work has involved collaborating with colleagues on the initial design of the language; making key technical breakthroughs leading to the first tractable semantics of the language; working out the semantics and theory of the language; and co-authoring numerous conference papers and technical reports describing the work.
Formally Verifying Conway's Lost Cosmological Theorem, 2006-2007
Independent research establishing a novel technique for verifying program properties using lazy evaluation. The work resulted in a new formal verification of a combinatorial theorem of J.H. Conway, and was achieved by applying my technique in the Haskell language. The work was presented at a seminar.
LolliMon Concurrent Linear Logic Programming Language, 2004-2005
Made major contributions to the design and analysis of LolliMon, a linear logic programming language. The work involved collaborating with colleagues on the initial design; developing a mathematical theory to specify the operational semantics of the language; and co-authoring a refereed conference paper describing the language and theory.
Made major contributions to Twelf, a theorem prover and specification checker based on the LF logical framework and the Elf logic programming language. This work included assimilating and comprehending a large existing code base; designing new algorithms and data structures for the key type reconstruction component of the software; implementing my design in the Standard ML language; constructing examples and test cases for the software distribution; walking other contributors through the implementation internals; and tracking and fixing defects.
Contributed to a research program aimed at creating a digital library of formal mathematical knowledge, using an open infrastructure based on logical frameworks to translate between knowledge developed in different theorem proving systems. My contributions included the preliminary design of a module system for LF; and participating in the project kickoff meeting at SRI International, Menlo Park.
Programming Language Design with Regions and Linear Types, 2001
With a colleague, designed a new memory management paradigm combining region-based memory management and linear types. My work included assimilating the relevant scientific literature; helping to elaborate the initial idea into the design of a new programming language incorporating the paradigm; developing the mathematical theory needed to specify the semantics of the language; co-authoring a refereed conference paper describing our work; and presenting our work at a conference in Florence, Italy.
Linear Logic Programming Language Implementation, 1996-1998
Redesigned and extended an implementation of Lolli, a logic programming language akin to Prolog, based on linear logic. This work involved reading and assimilating the scientific literature on linear logic and logic programming; designing novel algorithms and data structures for proof search in linear logic; implementing the algorithms in the Standard ML language; measuring and tuning the implementation for performance; visiting and collaborating with researchers at Kobe University, Japan, on aspects of the theory; and co-authoring a refereed conference paper describing the work.
Radiography Image Processing, 1997
As part of an Harvey Mudd CS Clinic team collaborating with Optivus Technology, Inc., contributed to the design and implementation of a tool for automatic radiographic image registration. My roles on the team included: researching techniques for image processing; design and implementation of novel de-noising algorithms.
Software Verification System Evaluation, 1996
As part of an Harvey Mudd Math Clinic team collaborating with the NASA Jet Propulsion Laboratory, surveyed and evaluated various approaches to formal software verification.
Routing Algorithms for Massively Parallel Computing, 1995-1996
Researched routing algorithms for wormhole routed massively-parallel computers under the direction of my advisor. This work involved designing new routing strategies; writing a large Monte Carlo simulation and visualization package in the C++ language in order to test the performance of the strategies; responding to the direction of the professor advising me and coordinating with his other students working on related projects; and co-authoring two refereed conference papers describing the work.
Graduate Research Fellowship, National Science Foundation, 1998-2001
Computer Science Department Class of '94 Award, Harvey Mudd College, 1998
Member of World Champion Team, ACM International Collegiate Programming Contest, 1997
Foundations of Programming Languages, Carnegie Mellon University, 1999 and 2005
Served as a teaching assistant and visiting lecturer for two instances of the undergraduate course on type systems and operational semantics of programming languages, taught in the Standard ML and Java languages.
Principles of Programming, Carnegie Mellon University, 2000
Served as head teaching assistant for the undergraduate course on functional and modular programming in the Standard ML language. The work included coordinating and supervising five undergraduate TAs.
ConCert Reading Group, Carnegie Mellon University
Envisioned and created the first student-run seminar in our research group. Each week the students participating read and discussed an academic paper. The group was managed by myself for the first two years and is still running.
Free Food Cam, Carnegie Mellon University
With a friend, designed and constructed custom hardware and software for a web cam installed in the department lounge soda machine, so grad students like myself could watch for leftover food from seminars, etc. as it arrived in the lounge. The system was based on a repurposed "web appliance", IP multicast, and VNC.
A list of publications and presentations is available online.