Introduction to ``Milestones in interactive theorem proving
From MaRDI portal
Cites work
- scientific article; zbMATH DE number 1701360 (Why is no real title available?)
- scientific article; zbMATH DE number 3776841 (Why is no real title available?)
- scientific article; zbMATH DE number 2003161 (Why is no real title available?)
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A verified compiler from Isabelle/HOL to CakeML
- Boolean unification - the story so far
- Concrete semantics. With Isabelle/HOL
- Equational reasoning in Isabelle
- Flyspeck I: Tame Graphs
- Higher-order unification, polymorphism, and subsorts
- Hoare logic for Java in Isabelle/HOL
- 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, J
- Linear quantifier elimination
- Logic for Programming, Artificial Intelligence, and Reasoning
- Modular higher-order E-unification
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Sledgehammer: judgement day
- Term Rewriting and All That
- Term rewriting and beyond -- theorem proving in Isabelle
- Types for Proofs and Programs
- Unification in Boolean rings
- Unification in primal algebras, their powers and their varieties
- Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
- Winskel is (almost) right: Towards a mechanized semantics textbook
Describes a project that uses
Uses Software
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)
