scholarly journals Program extraction applied to monadic parsing

2019 ◽  
Vol 29 (4) ◽  
pp. 487-518 ◽  
Author(s):  
Ulrich Berger ◽  
Alison Jones ◽  
Monika Seisenberger

Abstract This article outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using modified realizability, we extract formally verified and terminating programs from formal proofs. By extracting both primitive parsers and parser combinators, it is ensured that all complex parsers built from these are also correct, complete and terminating for any input. We demonstrate the viability of our approach by means of two case studies: we extract (i) a small arithmetic calculator and (ii) a non-deterministic natural language parser. The work is being carried out in the interactive proof system Minlog.

2001 ◽  
Vol 12 (04) ◽  
pp. 517-531
Author(s):  
OLEG VERBITSKY

The Parallel Repetition Theorem says that n-fold parallel execution of a two-prover one-round interactive proof system reduces the error probability exponentially in n. The bound on the error probability of the parallelized system depends on the error probability and the answer size of the single proof system. It is still unknown whether the theorem holds true with a bound depending only on the query size. This kind of a bound may be preferable whenever the query size is considerably smaller than the answer size, what really happens in some cryptographic protocols. Such a bound is only known in the case that queries to the provers are independent. The present paper extends this result to some cases of strong correlation between queries. In particular, a query-based variant of the Parallel Repetition Theorem is proven when the graph of dependence between queries to the provers is a tree and, in a bit weaker form, when this graph is a cycle.


2001 ◽  
Vol 8 (52) ◽  
Author(s):  
Jens Groth

We prove that a 3-move interactive proof system with the special soundness property made non-interactive by applying the Fiat-Shamir heuristic is almost a non-interactive proof of knowledge in the random oracle model. In an application of the result we demonstrate that the Damgård-Jurik voting scheme based on homomorphic threshold encryption is secure against a nonadaptive adversary according to Canetti's definition of multi-party computation security.


2016 ◽  
Vol 113 (31) ◽  
pp. 8618-8623 ◽  
Author(s):  
R. Scott Kemp ◽  
Areg Danagoulian ◽  
Ruaridh R. Macdonald ◽  
Jayson R. Vavrek

How does one prove a claim about a highly sensitive object such as a nuclear weapon without revealing information about the object? This paradox has challenged nuclear arms control for more than five decades. We present a mechanism in the form of an interactive proof system that can validate the structure and composition of an object, such as a nuclear warhead, to arbitrary precision without revealing either its structure or composition. We introduce a tomographic method that simultaneously resolves both the geometric and isotopic makeup of an object. We also introduce a method of protecting information using a provably secure cryptographic hash that does not rely on electronics or software. These techniques, when combined with a suitable protocol, constitute an interactive proof system that could reject hoax items and clear authentic warheads with excellent sensitivity in reasonably short measurement times.


2009 ◽  
Vol 9 (7&8) ◽  
pp. 648-656
Author(s):  
R. Cleve ◽  
D. Gavinsky ◽  
R. Jain

We show that every language in $\np$ is recognized by a two-prover interactive proof system with the following properties. The proof system is entanglement-resistant (i.e., its soundness is robust against provers who have prior shared entanglement), it has one round of interaction, the provers' answers are single bits, and the completeness-soundness gap is constant (formally, $\np\subseteq \xmips_{1-\varepsilon,1/2+\varepsilon}\mo[2]$, for any~$\varepsilon$ such that $0 < \varepsilon < 1/4$). Our result is based on the ``oracularizing" property of a particular private information retrieval scheme (PIR), and it suggests that investigating related properties of other PIRs might bear further fruit.


2014 ◽  
Vol 14 (5&6) ◽  
pp. 384-416
Author(s):  
Patrick Hayden ◽  
Kevin Milner ◽  
Mark M. Wilde

Suppose that a polynomial-time mixed-state quantum circuit, described as a sequence of local unitary interactions followed by a partial trace, generates a quantum state shared between two parties. One might then wonder, does this quantum circuit produce a state that is separable or entangled? Here, we give evidence that it is computationally hard to decide the answer to this question, even if one has access to the power of quantum computation. We begin by exhibiting a two-message quantum interactive proof system that can decide the answer to a promise version of the question. We then prove that the promise problem is hard for the class of promise problems with "quantum statistical zero knowledge" QSZK proof systems by demonstrating a polynomial-time Karp reduction from the QSZK-complete promise problem "quantum state distinguishability" to our quantum separability problem. By exploiting Knill's efficient encoding of a matrix description of a state into a description of a circuit to generate the state, we can show that our promise problem is NP-hard with respect to Cook reductions. Thus, the quantum separability problem (as phrased above) constitutes the first nontrivial promise problem decidable by a two-message quantum interactive proof system while being hard for both NP and QSZK. We also consider a variant of the problem, in which a given polynomial-time mixed-state quantum circuit accepts a quantum state as input, and the question is to decide if there is an input to this circuit which makes its output separable across some bipartite cut. We prove that this problem is a complete promise problem for the class QIP of problems decidable by quantum interactive proof systems. Finally, we show that a two-message quantum interactive proof system can also decide a multipartite generalization of the quantum separability problem.


Sign in / Sign up

Export Citation Format

Share Document