(*******************************************************************************
Project : Sumcheck Protocol
Authors : Azucena Garvia Bosshard < zucegb @ gmail . com >
Christoph Sprenger , ETH Zurich < sprenger @ inf . ethz . ch >
Jonathan Bootle , IBM Research Europe < jbt @ zurich . ibm . com >
*******************************************************************************)
chapter AFP
(*
Test the entry build using the command :
< isabelle > build - v - o browser_info - o " document = pdf " - o " document_variants = document : outline = / proof , / ML " - D < entry dir >
*)
session Sumcheck_Protocol (AFP) = "HOL-Probability" +
description ‹ Formalization of the Sumcheck Protocol›
options [timeout = 600 ]
sessions
"HOL-Library"
"HOL-Computational_Algebra"
"Polynomials"
directories
"Generalized_Sumcheck_Protocol"
"Instantiation_with_Polynomials"
theories
"Generalized_Sumcheck_Protocol/Probability_Tools"
"Generalized_Sumcheck_Protocol/Public_Coin_Proofs"
"Generalized_Sumcheck_Protocol/Substitutions"
"Generalized_Sumcheck_Protocol/Abstract_Multivariate_Polynomials"
"Generalized_Sumcheck_Protocol/Sumcheck_Protocol"
"Generalized_Sumcheck_Protocol/Completeness_Proof"
"Generalized_Sumcheck_Protocol/Soundness_Proof"
"Generalized_Sumcheck_Protocol/Sumcheck_as_Public_Coin_Proof"
"Instantiation_with_Polynomials/Polynomial_Instantiation"
"Instantiation_with_Polynomials/Univariate_Roots_Bound"
"Instantiation_with_Polynomials/Roots_Bounds"
"Instantiation_with_Polynomials/Concrete_Multivariate_Polynomials"
document_files
"root.tex" "session_graph.tex"
(* "root.bib" *)
Messung V0.5 in Prozent C=88 H=96 G=91
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-06-10)
¤
*© Formatika GbR, Deutschland