Types for Proofs and Programs

DOI10.1007/b98246zbMath1100.68620OpenAlexW4298423642MaRDI QIDQ5712318

Freek Wiedijk

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

Mechanization of proofs and logical operations (03B35)

Related Items

Four decades of {\textsc{Mizar}}. Foreword ⋮ Mizar: State-of-the-art and Beyond ⋮ The challenge of computer mathematics ⋮ A Brief Overview of Mizar ⋮ A proof-centric approach to mathematical assistants ⋮ A Declarative Language for the Coq Proof Assistant ⋮ Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book ⋮ Flexary connectives in Mizar ⋮ Prime simplicity ⋮ Translating between Language and Logic: What Is Easy and What Is Difficult ⋮ A Foundational View on Integration Problems ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF ⋮ Theorem proving as constraint solving with coherent logic ⋮ Computerizing Mathematical Text with MathLang ⋮ PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems

Uses Software

• Isabelle/Isar