Types for Proofs and Programs

DOI10.1007/B98246zbMath1100.68615OpenAlexW4298423642MaRDI QIDQ5712320

Clemens Ballarin

Publication date: 23 December 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

Related Items (20)

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

• Isabelle
• Isabelle/Isar
• Proof General

This page was built for publication: Types for Proofs and Programs