A Web Interface for Isabelle: The Next Generation

Lüth, Christoph; Ring, Martin

doi:10.1007/978-3-642-39320-4_22

A Web Interface for Isabelle: The Next Generation

Christoph Lüth²⁴ &
Martin Ring²⁴

Conference paper

958 Accesses
8 Citations

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7961))

Abstract

We present Clide , a web interface for the interactive theorem prover Isabelle. Clide uses latest web technology and the Isabelle/PIDE framework to implement a web-based interface for asynchronous proof document management that competes with, and in some aspects even surpasses, conventional user interfaces for Isabelle such as Proof General or Isabelle/jEdit.

This is a preview of subscription content, log in via an institution.

Chapter: USD 29.95; Price excludes VAT (USA)

eBook: USD 39.99; Price excludes VAT (USA)

Softcover Book: USD 54.99; Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

References

Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS, vol. 6824, pp. 244–259. Springer, Heidelberg (2011)
Chapter Google Scholar
Wenzel, M.: Isabelle/jEdit - a prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 468–471. Springer, Heidelberg (2012)
Chapter Google Scholar
Microsoft: Ux guidelines for windows store apps (November 2012), http://msdn.microsoft.com/en-us/library/windows/apps/hh465424.aspx .
Kaliszyk, C., Raamsdonk, F.V., Wiedijk, F., Hendriks, M., Vrijer, R.D.: Deduction using the ProofWeb system, http://prover.cs.ru.nl/
Aspinall, D.: Proof General: A generic tool for proof development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 38–42. Springer, Heidelberg (2000)
Chapter Google Scholar

Download references

Author information

Authors and Affiliations

Deutsches Forschungszentrum für Künstliche Intelligenz, Bremen, Germany
Christoph Lüth & Martin Ring

Authors

Christoph Lüth
View author publications
You can also search for this author in PubMed Google Scholar
Martin Ring
View author publications
You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, ON, Canada
Jacques Carette
School of Informatics, University of Edinburgh, 10 Crichton Street, EH8 9AB, Edinburgh, Scotland, UK
David Aspinall
School of Computer Science, University of Birmingham, Edgbaston, B15 2TT, Birmingham, UK
Christoph Lange
Faculty of Informatics, Department of Computer Graphics and Design, Masaryk University, Botanická 68a, 60200, Brno, Czech Republic
Petr Sojka
Johannes Kepler University Linz (JKU), RISC, Altenberger Strasse 69, 4040, Linz, Austria
Wolfgang Windsteiger

Rights and permissions

Reprints and permissions

Copyright information

About this paper

Cite this paper

Lüth, C., Ring, M. (2013). A Web Interface for Isabelle: The Next Generation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds) Intelligent Computer Mathematics. CICM 2013. Lecture Notes in Computer Science(), vol 7961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39320-4_22

Download citation

DOI: https://doi.org/10.1007/978-3-642-39320-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39319-8
Online ISBN: 978-3-642-39320-4
eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics