The following pages link to (Q4247084):
Displaying 10 items.
- A mechanized proof of the basic perturbation lemma (Q928666) (← 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)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- Formal reasoning under cached address translation (Q2209539) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- Interactive and automated proofs for graph transformations (Q4585009) (← links)