Related papers: Python client for Isabelle server
The Isabelle proof assistant includes a small functional language, which allows users to write and reason about programs. So far, these programs could be extracted into a number of functional languages: Standard ML, OCaml, Scala, and…
Despite being the most popular programming language, Python has not yet received enough attention from the community. To the best of our knowledge, there is no general static analysis framework proposed to facilitate the implementation of…
The Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable as technological basis for educational tools. The traditionally strong logical foundations of systems like HOL, Coq, or Isabelle have…
Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platform exemplifies this with its Isabelle/Scala systems…
Isabelle/PIDE is the current Prover IDE technology for Isabelle. It has been developed in ML and Scala in the past 4-5 years for this particular proof assistant, but with an open mind towards other systems. PIDE is based on an asynchronous…
PyCPL provides full access to ESO's Common Pipeline Library ( CPL) for astronomical data reduction within a Python environment. Not only does it offer a Python interface to the robust CPL library, but it also lets users and developers fully…
We propose an approach for searching for counterexamples of statements about algebraic structures with a medium-sized signature using the Isabelle proof assistant in an efficient, parallel manner. We contribute a Python client Isabelle…
We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle, for the teaching and learning of proofs and proving. The journey started from an attempt to use…
PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LCF-style provers like Isabelle (or Coq or HOL) with…
The purpose of this paper is to show how existing scientific software can be parallelized using a separate thin layer of Python code where all parallel communication is implemented. We provide specific examples on such layers of code, and…
Python has become the de-facto language for training deep neural networks, coupling a large suite of scientific computing libraries with efficient libraries for tensor computation such as PyTorch or TensorFlow. However, when models are used…
Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with…
This is an overview of the Isabelle technology behind the Archive of Formal Proofs (AFP). Interactive development and quasi-interactive build jobs impose significant demands of scalability on the logic (usually Isabelle/HOL), on Isabelle/ML…
OpenML is an online platform for open science collaboration in machine learning, used to share datasets and results of machine learning experiments. In this paper we introduce OpenML-Python, a client API for Python, opening up the OpenML…
We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low…
The use of Python is noticeably growing among the scientific community, and Astronomy is not an exception. The power of Python consists of being an extremely versatile high-level language, easy to program that combines both traditional…
Programmers may be hesitant to use declarative systems, because of the associated learning curve. In this paper, we present an API that integrates the IDP Knowledge Base system into the Python programming language. IDP is a state-of-the-art…
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized…
With the large diversity of platforms and devices used by students, web applications increasingly suggest themselves as the solution of choice. Developing adequate educational programming environments in the browser, however, remains a…
Existing profilers for scripting languages (a.k.a. "glue" languages) like Python suffer from numerous problems that drastically limit their usefulness. They impose order-of-magnitude overheads, report information at too coarse a…