HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Sat, 30 Nov 2019 23:26:47 GMT access-control-allow-origin: * etag: W/"5de2fab7-1412" expires: Mon, 29 Dec 2025 22:03:19 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: FA62:3FD64F:95CEC5:A810E4:6952F84F accept-ranges: bytes age: 0 date: Mon, 29 Dec 2025 21:53:19 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210060-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1767045200.638698,VS0,VE203 vary: Accept-Encoding x-fastly-request-id: 10094a78f77413e358e794f920132dbe9340e787 content-length: 2223

• Andrew M. Kent
• Software Researcher and Engineer
• Galois, Inc.
• Portland, Oregon

I'm a programming language and verification researcher/software engineer at Galois; I earned my Ph.D. at Indiana University under the advisement of Sam Tobin-Hochstadt.

My research interests revolve around programming languages and software engineering; in particular I frequently look for ways to leverage types, type theory, and formal verification techniques to build more robust systems.

Some work related to my dissertation has involved an extension to Typed Racket which adds support for basic dependent types. You can try it out by downloading Racket here (version >= 6.11).

Email | CV | Github | Twitter | Blog

Select Project Involvement

• Racket - In the past I have contributed to the programming language language Racket.
• Typed Racket - I helped maintain and improve Typed Racket (a typed dialect of Racket) for several years and added several features to the language (e.g. refinement types).

Publications

• Advanced Logical Type Systems for Untyped Languages, a dissertation. [pdf]
• Migratory Typing: Ten Years Later, with Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa, at SNAPL 2017. [pdf]
• Occurrence Typing Modulo Theories, with David Kempe and Sam Tobin-Hochstadt, at PLDI 2016. [acm | slides | arXiv]
• Design and Evaluation of Gradual Typing in Python, with Michael M. Vitousek, Jeremy G. Siek, and Jim Baker, at DLS 2014. [acm]
• Linking the Past: Discovering Historical Social Networks from Documents and Linking to a Geneological Database, with Douglas J. Kennard and William A. Barret, at HIP 2011. [acm]

Miscellaneous

• Down and Dirty with Semantic Set-theoretic Types (a tutorial) - A tutorial on how to implement the basic operations for semantic set-theoretic types. Included figures and pseudo-code is generated from a running redex model.