Types for Proofs and Programs
From MaRDI portal
Publication:5712320
DOI10.1007/b98246zbMath1100.68615MaRDI QIDQ5712320
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
Related Items
Psi-calculi in Isabelle, Balancing the load. Leveraging a semantics stack for systems verification, A proof-centric approach to mathematical assistants, Generating certified code from formal proofs: a case study in homological algebra, Partial and nested recursive function definitions in higher-order logic, Flyspeck II: The basic linear programs, The Isabelle Framework, Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL, Local Theory Specifications in Isabelle/Isar
Uses Software