Talk:Proof assistant

From Knowino

Jump to: navigation, search

	NOTICE, please do not remove from top of page.
	I released this article to Citizendium. In particular, the identical text that appears there is of my sole authorship. Therefore, no credit for Citizendium content on the Knowino applies.
	Boris Tsirelson 15:16, 18 December 2010 (EST)

Now available: Isabelle2011

Notable changes:

Experimental Prover IDE based on Isabelle/Scala and jEdit.
Coercive subtyping (configured in HOL/Complex_Main).
HOL code generation: Scala as another target language.
HOL: partial_function definitions.
HOL: various tool enhancements, including Quickcheck, Nitpick, Sledgehammer, SMT integration.
HOL: various additions to theory library, including HOL-Algebra, Imperative_HOL, Multivariate_Analysis, Probability.
HOLCF: reorganization of library and related tools.
HOL/SPARK: interactive proof environment for verification conditions generated by the SPARK Ada program verifier.
Improved Isabelle/Isar implementation manual (covering Isabelle/ML).