scholarly journals Program extraction applied to monadic parsing

2019 ◽  
Vol 29 (4) ◽  
pp. 487-518 ◽  
Author(s):  
Ulrich Berger ◽  
Alison Jones ◽  
Monika Seisenberger
Keyword(s):  
Natural Language ◽  
Case Studies ◽  
Proof System ◽  
Theoretic Approach ◽  
Formal Proofs ◽  
Interactive Proof ◽  
Program Extraction ◽  
Interactive Proof System

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.

REMARKS ON A QUERY-BASED VARIANT OF THE PARALLEL REPETITION THEOREM

2001 ◽  
Vol 12 (04) ◽  
pp. 517-531
Author(s):  
OLEG VERBITSKY
Keyword(s):  
Strong Correlation ◽  
Error Probability ◽  
Cryptographic Protocols ◽  
Parallel Execution ◽  
Proof System ◽  
Interactive Proof ◽  
Parallel Repetition ◽  
Interactive Proof System

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.

scholarly journals Extracting Witnesses from Proofs of Knowledge in the Random Oracle Model

2001 ◽  
Vol 8 (52) ◽  
Author(s):  
Jens Groth
Keyword(s):  
Random Oracle Model ◽  
Random Oracle ◽  
Proof System ◽  
Interactive Proof ◽  
Proof Of Knowledge ◽  
Proofs Of Knowledge ◽  
Voting Scheme ◽  
Definition Of ◽  
Interactive Proof System ◽  
Threshold Encryption

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.

scholarly journals Physical cryptographic verification of nuclear warheads

2016 ◽  
Vol 113 (31) ◽  
pp. 8618-8623 ◽  
Author(s):  
R. Scott Kemp ◽  
Areg Danagoulian ◽  
Ruaridh R. Macdonald ◽  
Jayson R. Vavrek
Keyword(s):  
Nuclear Weapon ◽  
Proof System ◽  
Interactive Proof ◽  
Highly Sensitive ◽  
Tomographic Method ◽  
Nuclear Arms Control ◽  
Arbitrary Precision ◽  
Interactive Proof System ◽  
Nuclear Warhead ◽  
Provably Secure

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.

A Low Communication Competitive Interactive Proof System for Promised Quadratic Residuosity

1996 ◽  
Vol 9 (2) ◽  
pp. 101
Author(s):  
Toshiya Itoh ◽  
Masafumi Hoshi ◽  
Shigeo Tsujii
Keyword(s):  
Proof System ◽  
Interactive Proof ◽  
Quadratic Residuosity ◽  
Interactive Proof System

Entanglement-resistant two-Prover interactive proof systems and non-adaptive PIRs

2009 ◽  
Vol 9 (7&8) ◽  
pp. 648-656
Author(s):  
R. Cleve ◽  
D. Gavinsky ◽  
R. Jain
Keyword(s):  
Information Retrieval ◽  
Private Information ◽  
Proof System ◽  
Private Information Retrieval ◽  
Interactive Proof ◽  
Interactive Proof Systems ◽  
Proof Systems ◽  
Retrieval Scheme ◽  
Interactive Proof System

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.

Two-message quantum interactive proofs and the quantum separability problem

2014 ◽  
Vol 14 (5&6) ◽  
pp. 384-416
Author(s):  
Patrick Hayden ◽  
Kevin Milner ◽  
Mark M. Wilde
Keyword(s):  
Quantum State ◽  
Polynomial Time ◽  
Mixed State ◽  
Quantum Circuit ◽  
Proof System ◽  
Interactive Proof ◽  
Proof Systems ◽  
Separability Problem ◽  
Promise Problems ◽  
Interactive Proof System

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