Introduction to ``Milestones in interactive theorem proving''
type: Item
instance of: scholarly article
title: Introduction to ``Milestones in interactive theorem proving''
zbMATH Open document ID: 1398.00118
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
full work available at URL: Avigad2018 IntroductionToMilestonesInInteractiveTheoremProving.pdf
Mathematics Subject Classification ID: 00B30
Mathematics Subject Classification ID: 68-06
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6921410
describes a project that uses: Isabelle/HOL
describes a project that uses: PIDE
describes a project that uses: Isabelle/jEdit
describes a project that uses: Flyspeck
describes a project that uses: Nitpick
describes a project that uses: Sledgehammer
describes a project that uses: Tame Graphs
describes a project that uses: CakeML
describes a project that uses: Locales
describes a project that uses: seL4
MaRDI profile type: Publication
OpenAlex ID: W2801537935
Wikidata QID: Q57382527
cites work: Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
cites work: Term Rewriting and All That
cites work: Types for Proofs and Programs
cites work: Q4736387
cites work: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
cites work: Sledgehammer: Judgement Day
cites work: A verified compiler from Isabelle/HOL to CakeML
cites work: Unification in Boolean rings
cites work: Boolean unification - the story so far
cites work: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
cites work: Equational reasoning in Isabelle
cites work: Term rewriting and beyond -- theorem proving in Isabelle
cites work: Unification in primal algebras, their powers and their varieties
cites work: Higher-order unification, polymorphism, and subsorts
cites work: Winskel is (almost) right: Towards a mechanized semantics textbook
cites work: Q2769440
cites work: Q4435474
cites work: Linear quantifier elimination
cites work: Flyspeck I: Tame Graphs
cites work: Concrete Semantics
cites work: Modular higher-order E-unification
cites work: Q3956381
cites work: Logic for Programming, Artificial Intelligence, and Reasoning
cites work: Hoare logic for Java in Isabelle/HOL
cites work: Q592091
DBLP publication ID: journals/jar/AvigadBKPPS18
DOI: 10.1007/S10817-018-9465-5
description: scientific article; zbMATH DE number 6921410