The Programatica Project
Integrating Programming, Properties and Validation

Intro People Papers Talks Tools Links

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
Valid HTML 4.01 Transitional
Thomas Hallgren