Browse Title Index


 
Issue Title
 
Vol 1, No 1 (2008) A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita Abstract   PDF (English)
Claudio Sacerdoti Coen, Enrico Tassi
 
Vol 5, No 1 (2012) A formal proof of Sasaki-Murao algorithm Abstract   PDF (English)
Thierry Coquand, Anders Mörtberg, Vincent Siles
 
Vol 6, No 1 (2013) A Formal Proof of Square Root and Division Elimination in Embedded Programs Abstract   PDF (English)
Pierre Neron
 
Vol 4, No 1 (2011) A Formal Proof Of The Riesz Representation Theorem Abstract   PDF (English)
Anthony Narkawicz
 
Vol 8, No 1 (2015) A formal verification of the theory of parity complexes Abstract   PDF (English)
Mitchell Buckley
 
Vol 1, No 1 (2008) A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language Abstract   PDF (English)
Andre Luiz Galdino, Mauricio Ayala-Rincón
 
Vol 2, No 1 (2009) A formalized proof of Dirichlet's theorem on primes in arithmetic progression Abstract   PDF (English)
John Harrison
 
Vol 2, No 1 (2009) A New Look at Generalized Rewriting in Type Theory Abstract   PDF (English)
Matthieu Sozeau
 
Vol 1, No 1 (2008) A Page in Number Theory Abstract   PDF (English)
Andrea Asperti, Cristian Armentano
 
Vol 5, No 1 (2012) A proof of Bertrand's postulate Abstract   PDF (English)
Andrea Asperti, Wilmer Ricciotti
 
Vol 4, No 1 (2011) A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration Abstract   PDF (English)
Luca Chiarabini, Olivier Danvy
 
Vol 6, No 1 (2013) A String of Pearls: Proofs of Fermat's Little Theorem Abstract   PDF (English)
Hing Lun Chan, Michael Norrish
 
Vol 7, No 2 (2014): Special Issue: User Tutorials 2 Abella: A System for Reasoning about Relational Specifications Abstract   PDF (English)
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
 
Vol 7, No 1 (2014) An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing Abstract   PDF (English)
Reynald Affeldt, Kazuhiko Sakaguchi
 
Vol 3, No 2 (2010): Special Issue: User Tutorials I An Introduction to Programming and Proving with Dependent Types in Coq Abstract   PDF (English)
Adam Chlipala
 
Vol 3, No 2 (2010): Special Issue: User Tutorials I An introduction to small scale reflection in Coq Abstract   PDF (English)
Georges Gonthier, Assia Mahboubi
 
Vol 3, No 1 (2010) Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure Abstract   PDF (English)
Geoff Sutcliffe, Christoph Benzmueller
 
Vol 3, No 1 (2010) Basic first-order model theory in Mizar Abstract   PDF (English)
Marco Bright Caminati
 
Vol 7, No 1 (2014) Certified Kruskal's Tree Theorem Abstract   PDF (English)
Christian Sternagel
 
Vol 2, No 1 (2009) Computing with Classical Real Numbers Abstract   PDF (English)
Cezary Kaliszyk, Russell O'Connor
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Conversion of HOL Light proofs into Metamath Abstract   PDF (English)
Mario M Carneiro
 
Vol 8, No 1 (2015) Formal Proofs for Nonlinear Optimization Abstract   PDF (English)
Victor Magron, Xavier Allamigeon, Stéphane Gaubert, Benjamin Werner
 
Vol 6, No 1 (2013) Formal Verification of Language-Based Concurrent Noninterference Abstract   PDF (English)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
 
Vol 6, No 1 (2013) Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model Abstract   PDF (English)
Mauricio Ayala-Rincón, Yuri Santos Rego
 
Vol 2, No 1 (2009) Formalization of the Integral Calculus in the PVS Theorem Prover Abstract   PDF (English)
Ricky Wayne Butler
 
Vol 9, No 2 (2016) Formalization of the pumping lemma for context-free languages Abstract   PDF (English)
Marcus V M Ramos, José Carlos Bacelar Almeida, Nelma Moreira, Ruy José Guerra Barretto de Queiroz
 
Vol 4, No 1 (2011) Formalizing a Proof that e is Transcendental Abstract   PDF (English)
Jesse Bingham
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Formalizing Scientifically Applicable Mathematics in a Definitional Framework Abstract   PDF (English)
Arnon Avron, Liron Cohen
 
Vol 1, No 1 (2008) Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator Abstract   PDF (English)
Concepción Vidal, Felicidad Aguado, José Luis Doncel, Jose María Molinelli, Gilberto Perez
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Hammering towards QED Abstract   PDF (English)
Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
 
Vol 3, No 1 (2010) Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets Abstract   PDF (English)
José Grimm
 
Vol 9, No 2 (2016) Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers Abstract   PDF (English)
José Grimm
 
Vol 4, No 1 (2011) Initial Semantics for higher-order typed syntax in Coq Abstract   PDF (English)
Benedikt Ahrens, Julianna Zsido
 
Vol 8, No 2 (2015): Special Issue - PhD Theses Initiality for Typed Syntax and Semantics Abstract   PDF (English)
Benedikt Ahrens
 
Vol 7, No 1 (2014) Innocuous Double Rounding of Basic Arithmetic Operations Abstract   PDF (English)
Pierre Roux
 
Vol 9, No 2 (2016) Lawvere-Tierney sheafification in Homotopy Type Theory Abstract   PDF (English)
Kevin Quirin, Nicolas Tabareau
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Mathematical Text Processing in EA-style: a Sequent Aspect Abstract   PDF (English)
Alexander Lyaletski
 
Vol 7, No 2 (2014): Special Issue: User Tutorials 2 Matita Tutorial Abstract   PDF (English)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Mixing Computations and Proofs Abstract   PDF (English)
Michael Beeson
 
Vol 3, No 2 (2010): Special Issue: User Tutorials I Mizar in a Nutshell Abstract   PDF (English)
Adam Grabowski, Artur Kornilowicz, Adam Naumowicz
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Now f is continuous (exercise!) Abstract   PDF (English)
Robin Denis Arthan
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Preface: Twenty Years of the QED Manifesto Abstract   PDF (English)
John Harrison, Josef Urban, Freek Wiedijk
 
Vol 8, No 1 (2015) Programming type-safe transformations using higher-order abstract syntax Abstract   PDF (English)
Olivier Savary Belanger, Stefan Monnier, Brigitte Pientka
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Proof Auditing Formalised Mathematics Abstract   PDF (English)
Mark Miles Adams
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge Abstract   PDF (English)
Michael Kohlhase, Florian Rabe
 
Vol 7, No 1 (2014) Relative Monads Formalised Abstract   PDF (English)
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
 
Vol 3, No 1 (2010) Sets in Coq, Coq in Sets Abstract   PDF (English)
Bruno Barras
 
Vol 5, No 1 (2012) Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover Abstract   PDF (English)
Ferruccio Guidi
 
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto Theorema 2.0: Computer-Assisted Natural-Style Mathematics Abstract   PDF (English)
Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger
 
Vol 9, No 2 (2016) Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC Abstract   PDF (English)
YuHui Lin, Gudmund Grov, Rob Arthan
 
1 - 50 of 52 Items 1 2 > >>