A Formal Proof of the Expressiveness of Deep Learning (English)
- New search for: Bentkamp, Alexander
- New search for: Blanchette, Jasmin Christian
- New search for: Klakow, Dietrich
- New search for: Ayala-Rincón, Mauricio
- Further information on Ayala-Rincón, Mauricio:
- https://orcid.org/http://orcid.org/0000-0003-0089-3905
- New search for: Muñoz, César A.
- New search for: Bentkamp, Alexander
- New search for: Blanchette, Jasmin Christian
- New search for: Klakow, Dietrich
In:
Interactive Theorem Proving
: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings
;
Chapter: 4
;
46-64
;
2017
- Article/Chapter (Book) / Electronic Resource
-
Title:A Formal Proof of the Expressiveness of Deep Learning
-
Additional title:Lect.Notes Computer
-
Contributors:Ayala-Rincón, Mauricio ( editor ) / Muñoz, César A. ( editor ) / Bentkamp, Alexander ( author ) / Blanchette, Jasmin Christian ( author ) / Klakow, Dietrich ( author )
-
Conference:International Conference on Interactive Theorem Proving ; 2017 ; Brasília, Brazil
-
Published in:Interactive Theorem Proving : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings ; Chapter: 4 ; 46-64Lecture Notes in Computer Science ; 10499 ; 46-64
-
Publisher:
- New search for: Springer International Publishing
-
Place of publication:Cham
-
Publication date:2017-01-01
-
Size:19 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Article/Chapter (Book)
-
Type of material:Electronic Resource
-
Language:English
-
Keywords:
-
Source:
Table of contents eBook
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
Automated Theory Exploration for Interactive Theorem Proving:Johansson, Moa et al. | 2017
- 2
-
Automating Formalization by Statistical and Semantic Parsing of MathematicsKaliszyk, Cezary / Urban, Josef / Vyskočil, Jiří et al. | 2017
- 3
-
A Formalization of Convex Polyhedra Based on the Simplex MethodAllamigeon, Xavier / Katz, Ricardo D. et al. | 2017
- 4
-
A Formal Proof of the Expressiveness of Deep LearningBentkamp, Alexander / Blanchette, Jasmin Christian / Klakow, Dietrich et al. | 2017
- 5
-
Formalization of the Lindemann-Weierstrass TheoremBernard, Sophie et al. | 2017
- 6
-
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer SemanticsBesson, Frédéric / Blazy, Sandrine / Wilke, Pierre et al. | 2017
- 7
-
Formal Verification of a Floating-Point Expansion Renormalization AlgorithmBoldo, Sylvie / Joldes, Mioara / Muller, Jean-Michel / Popescu, Valentina et al. | 2017
- 8
-
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party ComputationButler, David / Aspinall, David / Gascón, Adrià et al. | 2017
- 9
-
FoCaLiZe and Dedukti to the Rescue for Proof InteroperabilityCauderlier, Raphaël / Dubois, Catherine et al. | 2017
- 10
-
A Formal Proof in Coq of LaSalle’s Invariance PrincipleCohen, Cyril / Rouhling, Damien et al. | 2017
- 11
-
How to Get More Out of Your OraclesCruz-Filipe, Luís / Larsen, Kim S. / Schneider-Kamp, Peter et al. | 2017
- 12
-
Certifying Standard and Stratified Datalog Inference Engines in SSReflectBenzaken, Véronique / Contejean, Évelyne / Dumbrava, Stefania et al. | 2017
- 13
-
Weak Call-by-Value Lambda Calculus as a Model of Computation in CoqForster, Yannick / Smolka, Gert et al. | 2017
- 14
-
Bellerophon: Tactical Theorem Proving for Hybrid SystemsFulton, Nathan / Mitsch, Stefan / Bohrer, Rose / Platzer, André et al. | 2017
- 15
-
Formalizing Basic Quaternionic AnalysisGabrielli, Andrea / Maggesi, Marco et al. | 2017
- 16
-
A Formalized General Theory of Syntax with BindingsGheri, Lorenzo / Popescu, Andrei et al. | 2017
- 17
-
Proof Certificates in PVSGilbert, Frédéric et al. | 2017
- 18
-
Efficient, Verified Checking of Propositional ProofsHeule, Marijn / Hunt, Warren / Kaufmann, Matt / Wetzler, Nathan et al. | 2017
- 19
-
Proof Tactics for Assertions in Separation LogicHóu, Zhé / Sanán, David / Tiu, Alwen / Liu, Yang et al. | 2017
- 20
-
Categoricity Results for Second-Order ZF in Dependent Type TheoryKirst, Dominik / Smolka, Gert et al. | 2017
- 21
-
Making PVS Accessible to Generic Services by Interpretation in a Universal FormatKohlhase, Michael / Müller, Dennis / Owre, Sam / Rabe, Florian et al. | 2017
- 22
-
Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft DynamicsKouskoulas, Yanni / Genin, Daniel / Schmidt, Aurora / Jeannin, Jean-Baptiste et al. | 2017
- 23
-
Using Abstract Stobjs in ACL2 to Compute Matrix Normal FormsLambán, Laureano / Martín-Mateos, Francisco J. / Rubio, Julio / Ruiz-Reina, José-Luis et al. | 2017
- 24
-
Typing Total Recursive Functions in CoqLarchey-Wendling, Dominique et al. | 2017
- 25
-
Effect Polymorphism in Higher-Order Logic (Proof Pearl)Lochbihler, Andreas et al. | 2017
- 26
-
Schulze Voting as Evidence Carrying ComputationPattinson, Dirk / Tiwari, Mukesh et al. | 2017
- 27
-
Verified Spilling and Translation Validation with RepairRosemann, Julian / Schneider, Sigurd / Hack, Sebastian et al. | 2017
- 28
-
A Verified Generational Garbage Collector for CakeMLSandberg Ericsson, Adam / Myreen, Magnus O. / Åman Pohjola, Johannes et al. | 2017
- 29
-
A Formalisation of Consistent Consequence for Boolean Equation Systemsvan Delft, Myrthe / Geuvers, Herman / Willemse, Tim A. C. et al. | 2017
- 30
-
Homotopy Type Theory in Leanvan Doorn, Floris / von Raumer, Jakob / Buchholtz, Ulrik et al. | 2017
- 31
-
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyZakowski, Yannick / Cachera, David / Demange, Delphine / Petri, Gustavo / Pichardie, David / Jagannathan, Suresh / Vitek, Jan et al. | 2017
- 32
-
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2Zhan, Bohua et al. | 2017