Introduction to ``Milestones in interactive theorem proving

DOI10.1007/S10817-018-9465-5zbMATH Open1398.00118DBLPjournals/jar/AvigadBKPPS18OpenAlexW2801537935WikidataQ57382527 ScholiaQ57382527MaRDI QIDQ1663212FDOQ1663212

Author name not available (Why is that?)

Publication date: 21 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://research.vu.nl/ws/files/118674118/Avigad2018_IntroductionToMilestonesInInteractiveTheoremProving.pdf

Mathematics Subject Classification ID

Festschriften (00B30) Proceedings, conferences, collections, etc. pertaining to computer science (68-06)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Flyspeck I: Tame Graphs
• Term Rewriting and All That
• Equational reasoning in Isabelle
• Concrete Semantics
• Types for Proofs and Programs
• Sledgehammer: Judgement Day
• Unification in Boolean rings
• Boolean unification - the story so far
• Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
• Hoare logic for Java in Isabelle/HOL
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Linear quantifier elimination
• Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8--13, 2012. Proceedings
• Unification in primal algebras, their powers and their varieties
• Logic for Programming, Artificial Intelligence, and Reasoning
• A verified compiler from Isabelle/HOL to CakeML
• Modular higher-order E-unification
• Higher-order unification, polymorphism, and subsorts
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Term rewriting and beyond -- theorem proving in Isabelle

Cited In (1)

• A proof system for graph (non)-isomorphism verification

Uses Software

• Nitpick
• Isabelle/HOL
• PIDE
• Isabelle/jEdit
• Sledgehammer
• CakeML
• Flyspeck
• Locales
• seL4
• Tame Graphs

This page was built for publication: Introduction to ``Milestones in interactive theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663212)