Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Isabelle/HOL
Isabelle/HOL - Isabelle/HOL
Date of the last release: 01 December 2013

Person in charge : WENZEL Markus


Isabelle is one of the top five interactive theorem proving systems. It is used in numerous academic projects on formal theory development (Kepler Conjecture, Prime Number Theorem) and a few major industrial verifications (NICTA Verification of the L4 Kernel). Isabelle is jointly developed at University of Cambridge, Technische Universität München and Université Paris-Sud. The development at UPSud is focussed on the parallelization of the prover kernel and the development of asynchronous proof checking facilities and the development of new Prover IDE exploiting these features.

More information: http://www.cl.cam.ac.uk/research/hvg/isabelle/

Software - Licence : BSD License



Research activities
  Formalisation of (Specification and Programming) Languages in Proof Assistants

Members
  WENZEL Markus

Group
  Verification of Algorithms, Languages and Systems

Software & patents
DNADNA
Deep Neural Architectures for DNA

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas