The following pages link to Types for Proofs and Programs (Q5712320):
Displaying 21 items.
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- A modular first formalisation of combinatorial design theory (Q2128787) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Locales: a module system for mathematical theories (Q2352487) (← links)
- Flyspeck II: The basic linear programs (Q2379683) (← links)
- The Isabelle Framework (Q3543647) (← links)
- Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL (Q3543667) (← links)
- Local Theory Specifications in Isabelle/Isar (Q3638251) (← links)
- Psi-calculi in Isabelle (Q5890661) (← links)
- Psi-calculi in Isabelle (Q5895110) (← links)
- Formally verified animation for RoboChart using interaction trees (Q6151624) (← links)
- APML: an architecture proof modeling language (Q6535972) (← links)
