Quelle  ROOT

(*******************************************************************************

  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 \<open>Formalization of the Sumcheck Protocol\<close> 

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" *)