¡¿ NATHAN COLLINS IS ON THE INTERNET ?!

Yes, it's a very exclusive club ...
[Chicago at night]

~ About Me ~

I'm an nth-year PhD student at Portland State University, studying programming languages, type theory, and interactive theorem proving.

Before coming to Portland State I earned a master's in mathematics at the University of Wisconsin, Madison, and did a funded internet startup in Pittsburgh, Pennsylvania.

I do a lot of coding, recently in Haskell, Python, and Bash/ZSH. Some of my work is hosted publicly on GitHub (ntc2), Google Code (nathan.collins), and Bitbucket (ntc2). I'm active on Stack Overflow (ntc2).

~ Contact Info ~

FAB 115-05
Dept of Computer Science
Portland State University
Portland, OR 97207
<nathan.collins, one of those little circles with the a in it, gmail.com>

~ Research ~

I'm currently working with Tim Sheard and Larry Diehl on Spire, a dependently typed programming language with native support for generic programming.

Before that I worked with Andrew Tolmach and many others on the CRASH/SAFE project. Specifically, I worked on the machine-language implementation and Coq verification of a dynamic-information-flow firmware.

Before that I interned at Microsoft Research Cambridge with Dimitrios Vytiniotis and Simon Peyton Jones, and along with Koen Claessen, and Charles-Pierre Astolfi we designed and implemented a statically checked contract system – a limited form of dependent types – for Haskell.

Before that I worked with Tim Sheard (and many others) on Trellys, a "practical" dependently typed programming language.

~ Publications ~

A Verified Information-Flow Architecture
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach.
In Principles of Programming Languages (POPL), 2014.
[ Paper ∧ Coq development ]

Equational Reasoning about Programs with General Recursion and Call-by-value Semantics
Garrin Kimmel, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathin Collins, and Ki Yung Anh.
In Progress in Informatics, (10), 2013.
[ Paper ]

Static Contract Checking via First-Order Logic
Nathan Collins.
Portland State University Research Proficiency Exam, 2012.
[ Paper ∨ Slides ]
(The text of the paper is completely my work – as required for the RPE – but the work reported was mostly performed during an internship at Microsoft Research Cambridge and is joint with Charles-Pierre Astolfi, Koen Claessen, Simon Peyton Jones, and Dimitrios Vytiniotis.)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich.
In Mathematically Structured Functional Programming (MSFP), 2012.
[ Paper ]

Equational Reasoning about Programs with General Recursion and Call-by-value Semantics
Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and Ki Yung Ahn.
In Programming Languages meets Program Verification (PLPV), 2012.
[ Paper ]