Related papers: Pervasive Parallelism in Highly-Trustable Interact…
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an…
This paper presents an efficient parallel approximation scheme for a new class of min-max problems. The algorithm is derived from the matrix multiplicative weights update method and can be used to find near-optimal strategies for…
In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct…
We present a model of multithreaded computation, combining fork-join and single-instruction-multiple-data parallelisms, with an emphasis on estimating parallelism overheads of programs written for modern many-core architectures. We…
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation…
In this chapter, we show why parallel MATLAB is useful, provide a comparison of the different parallel MATLAB choices, and describe a number of applications in Signal and Image Processing: Audio Signal Processing, Synthetic Aperture Radar…
It has been shown that a class of probabilistic domain models cannot be learned correctly by several existing algorithms which employ a single-link look ahead search. When a multi-link look ahead search is used, the computational complexity…
The paradigm of Tabled Logic Programming (TLP) is now supported by a number of Prolog systems, including XSB, YAP Prolog, B-Prolog, Mercury, ALS, and Ciao. The reasons for this are partly theoretical: tabling ensures termination and optimal…
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and…
We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good…
This paper presents an efficient adaptation and application of the Dempster-Shafer theory of evidence, one that can be used effectively in a massively parallel hierarchical system for visual pattern perception. It describes the techniques…
We study the problem of verifiable polynomial evaluation in the user-server and multi-party setups. We propose {INTERPOL}, an information-theoretically verifiable algorithm that allows a user to delegate the evaluation of a polynomial to a…
We propose a new computational framework that combines the recently developed time-parallel (TP) and the compound wavelet matrix (CWM) methods. The framework, termed tpCWM, offers significant computational acceleration by making…
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal…
This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facility with which the model can be extended to incorporate…
This volume contains the proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010) which took place on July 15 in Edinburgh, UK. This workshop was held as a satellite workshop of the International…
Due to their "inherent parallelism", interaction nets have since their introduction been considered as an attractive implementation mechanism for functional programming. We show that a simple highly-concurrent implementation in Haskell can…
For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are generally kept relatively small. On top of the kernel, additional symbols and inference rules are defined. This paper presents an analysis of how kernel…
A new high-level interface to multi-threading in Prolog, implemented in hProlog, is described. Modern CPUs often contain multiple cores and through high-level multi-threading a programmer can leverage this power without having to worry…
Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theorem provers. Recent…