The Programatica Project

Research Papers

Axiomatic Constructor Classes in Isabelle/HOLCF: Brian Huffman, John Matthews and Peter White. (TPHOLs 2005)
A Principled Approach to Operating System Construction in Haskell: Thomas Hallgren, Mark P. Jones, Rebekah Leslie, Andrew Tolmach. (ICFP 2005)
Dynamic Intransitive Noninterference: Rebekah Leslie. (ISSSE 2006)

Automated Soundness Checking of a Programming Logic for Haskell: Richard B. Kieburtz
Canonization for Disjoint Union of Theories: Sava Krstic and Sylvain Conchon
Domain Separation by Construction: William Harrison, Mark Tullsen, and James Hook
Fine Control of Demand in Haskell: William Harrison, Tim Sheard, and Jim Hook
A Formal Specification for the Haskell 98 Module System: Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren, 2002
Haskell Tools from the Programatica Project - Demo Abstract: Thomas Hallgren, 2003
Inductive Invariants for Nested Recursion: Sava Krstic and John Matthews, 2003
A Lexer for Haskell in Haskell: Thomas Hallgren, 2003
The Logic of Demand in Haskell: William Harrison and Richard Kieburtz
Pattern-driven reduction in Haskell: William Harrison and Richard B. Kieburtz, 2002
P-logic: Property Verification for Haskell Programs: Richard B. Kieburtz, 2002
Programatica Tools for Certifiable, Auditable Development of High-assurance Systems in Haskell: The Programatica Team
Reflecting Demand in Programming Logics: a case study for Haskell: William Harrison and Richard B. Kieburtz
Strategies for Combining Decision Procedures: Sylvain Conchon, Sava Krstic