TRELLYS: The TRELLYS
project seeks to design a
dependently-typed programming language that
supports both programming
and theorem proving in the same framework.
State) and Tim
(Portland State), we have been discovering
it means for programs and proofs to interact.
See our POPL 2014 paper, as well as papers in MSFP2012
2012. Also, slides from PLPV
2010 and RDP
2011, give an
overview of our work.
In 2013 and 2014, I presented a tutorial on designing dependently-typed
languages at the Oregon Programming Languages Summer School.
Haskell: this project works to extend the type
system of Haskell with better support for
dependently-typed programing. My primary collaborators for this project are
Simon Peyton Jones and Dimitrios Vytiniotis at MSR Cambridge, and Penn
student Richard Eisenberg.
for programming languages research:
Designing and proving
properties about programming languages is hard,
but the proofs
themselves are straightforward once you know how
to set them up. At the
same time, it is all too easy to miss the one
little case that ruins
whole "proof". Modern proof assistants, such as
Coq, and Isabelle
are good at expressing this sort of reasoning,
but it is hard to
know where to start. I've been working with the
problems, organize a workshop,
binding, and develop educational
materials about mechanizing programming
language metatheory. Brian
Aydemir developed a library
programming language metatheory (used in the
Penn tutorials) and LNgen,
tool for automatically proving properties about