The High-Assurance Systems Programming (HASP) project at Portland State University (a joint project with Galois, Inc.) is an ongoing research project that began in 2008.
HASP has the following three major research goals:
Experience Report: Using Hackage to Inform Language Design. J. Garrett Morris. Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell (Haskell '10), Baltimore, Maryland, USA, September, 2010.
Instance Chains: Type Class Programming Without Overlapping Instances. J. Garrett Morris and Mark P. Jones. Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, Maryland, USA, September, 2010.
A Certified Framework for Compiling and Executing Garbage-Collected Languages. Andrew McCreight, Tim Chevalier, and Andrew Tolmach. Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, Maryland, USA, September, 2010.
A New Foundation for Nominal Isabelle. Brian Huffman and Christian Urban. Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP '10), Edinburgh, UK, July 2010.
Verifying Separation for a Monadic Scheduler. Tom Harke. In Proceedings of the 2009 CALCO Young Researchers Workshop (CALCO-jnr '09), Udine, Italy, September, 2009.
A Purely Definitional Universal Domain. Brian Huffman. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLS '09), Munich, Germany, August, 2009.
Practical Tactics for Separation Logic. Andrew McCreight. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLS '09), Munich, Germany, August, 2009. (associated Coq development)
Reasoning with Powerdomains in Isabelle/HOLCF. Brian Huffman. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLS '08) (Emerging Trends), Montreal, Quebec, Canada, August, 2008.
Language and Program Design for Functional Dependencies. Mark P. Jones and Iavor Diatchki. In Proceedings of the ACM Haskell Symposium (Haskell '08), Victoria, British Columbia, Canada, September 25, 2008.
We have openings for PhD students in 2011 and 2012. If you are interested in Haskell, functional programming, programming language theory, and/or systems programming, then consider applying to Portland State's doctoral program in computer science and working with our group. For more information, contact James Hook.
You need not wait until you are admitted before contacting us: in particular, we may have funding available for potential students to visit PSU at any time.