NDLI: Formalization of Shannon’s Theorems

Content Provider	Springer Nature Link
Author	Affeldt, Reynald Hagiwara, Manabu Sénizergues, Jonas
Copyright Year	2013
Abstract	The most fundamental results of information theory are Shannon’s theorems. These theorems express the bounds for (1) reliable data compression and (2) data transmission over a noisy channel. Their proofs are non-trivial but are rarely detailed, even in the introductory literature. This lack of formal foundations is all the more unfortunate that crucial results in computer security rely solely on information theory: this is the so-called “unconditional security”. In this article, we report on the formalization of a library for information theory in the SSReflect extension of the Coq proof-assistant. In particular, we produce the first formal proofs of the source coding theorem, that introduces the entropy as the bound for lossless compression, and of the channel coding theorem, that introduces the capacity as the bound for reliable communication over a noisy channel.
Starting Page	63
Ending Page	103
Page Count	41
File Format	PDF
ISSN	01687433
Journal	Journal of Automated Reasoning
Volume Number	53
Issue Number	1
e-ISSN	15730670
Language	English
Publisher	Springer Netherlands
Publisher Date	2013-12-11
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Information theory Shannon’s theorems Noisy-channel coding theorem Coq SSReflect Mathematical Logic and Formal Languages Artificial Intelligence (incl. Robotics) Mathematical Logic and Foundations Symbolic and Algebraic Manipulation
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Computational Theory and Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

Formal Power Series

Completeness and Decidability Results for CTL in Constructive Type Theory

A Formalization of the Knuth–Bendix(–Huet) Critical Pair Theorem

Theorem Proving Modulo

Theorem of Three Circles in Coq

Formalizing an Analytic Proof of the Prime Number Theorem

Reverse Complexity

Strongly Typed Term Representations in Coq

Formalization of Shannon’s Theorems

Similar Documents

A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

Formal Power Series

Completeness and Decidability Results for CTL in Constructive Type Theory

A Formalization of the Knuth–Bendix(–Huet) Critical Pair Theorem

Theorem Proving Modulo

Theorem of Three Circles in Coq

Formalizing an Analytic Proof of the Prime Number Theorem

Reverse Complexity

Strongly Typed Term Representations in Coq

Formalization of Shannon’s Theorems