Types for Proofs and Programs

Related Items

A modular first formalisation of combinatorial design theory, Eisbach: a proof method language for Isabelle, Balancing the load. Leveraging a semantics stack for systems verification, Flyspeck II: The basic linear programs, A proof-centric approach to mathematical assistants, Introduction to ``Milestones in interactive theorem proving, Formally verified animation for RoboChart using interaction trees, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Exploring the structure of an algebra text with locales, Psi-calculi in Isabelle, Psi-calculi in Isabelle, The Isabelle Framework, Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL, Verification and code generation for invariant diagrams in Isabelle, Generating certified code from formal proofs: a case study in homological algebra, Partial and nested recursive function definitions in higher-order logic, Local Theory Specifications in Isabelle/Isar, Interactive verification of architectural design patterns in FACTum, A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory, Locales: a module system for mathematical theories

Uses Software