×

Journal of Formalized Reasoning

Short Title: J. Formaliz. Reason.
Publisher: Università di Bologna, CIB Centro Inter-Bibliotecario, Bologna
ISSN: 1972-5787/e
Online: http://jfr.cib.unibo.it/issue/archive
Comments: Journal; Indexed cover-to-cover; Published electronic only as of Vol. 1 (2008). This journal is available open access.
Documents Indexed: 64 Publications (since 2008)
References Indexed: 15 Publications with 540 References.
all top 5

Authors

3 Asperti, Andrea
3 Bertot, Yves
2 Affeldt, Reynald
2 Ahrens, Benedikt
2 Appel, Andrew W.
2 Ayala-Rincón, Mauricio
2 Chapman, James T. E.
2 Grimm, José
2 Guidi, Ferruccio
2 Kaliszyk, Cezary
2 Narkawicz, Anthony Joseph
2 Ricciotti, Wilmer
2 Sacerdoti Coen, Claudio
2 Urban, Josef
2 Uustalu, Tarmo
1 Aguado, Felicidad
1 Alessi, Fabio
1 Allais, Guillaume
1 Allamigeon, Xavier
1 Altenkirch, Thorsten
1 Armentano, Cristian
1 Arthan, Rob D.
1 Arthan, Robin Denis
1 Avron, Arnon
1 Bacelar Almeida, José
1 Baelde, David
1 Bagnall, Alexander
1 Barras, Bruno
1 Beeson, Michael J.
1 Benzmüller, Christoph Ewald
1 Bingham, Jesse D.
1 Blanchette, Jasmin Christian
1 Buchberger, Bruno
1 Buckley, Mitchell
1 Butler, Ricky Wayne
1 Caminati, Marco Bright
1 Carneiro, Mario M.
1 Chan, Hing-Lun
1 Chaudhuri, Kaustuv
1 Chen, Ran
1 Chiarabini, Luca
1 Ciaffaglione, Alberto
1 Clochard, Martin
1 Cohen, Cyril
1 Cohen, Liron
1 Coquand, Thierry
1 Danvy, Olivier
1 De Queiroz, Ruy José Guerra Barretto
1 De Rauglaudre, Daniel
1 Di Gianantonio, Pietro
1 Doncel, José Luis
1 Dutle, Aaron M.
1 Gacek, Andrew
1 Galdino, André Luiz
1 Gaubert, Stéphane
1 Gonthier, Georges
1 Grabowski, Adam
1 Grov, Gudmund
1 Hölzl, Johannes
1 Honsell, Furio
1 Jebelean, Tudor
1 Kohlhase, Michael
1 Korniłowicz, Artur
1 Kutsia, Temur
1 Lenisa, Marina
1 Lescanne, Pierre
1 Lin, Yuhui
1 Magron, Victor
1 Mahboubi, Assia
1 Maletzky, Alexander
1 Marché, Claude
1 Merten, Samuel
1 Miller, Dale Allen
1 Molinelli, Jose María
1 Monnier, Stefan
1 Moreira, Nelma
1 Mörtberg, Anders
1 Muñoz, César A.
1 Nadathur, Gopalan
1 Naumowicz, Adam
1 Neron, Pierre
1 Nipkow, Tobias
1 Norrish, Michael
1 O’Connor, Russell
1 Padmanabhan, Ranganathan
1 Paulson, Lawrence Charles
1 Pérez, Gilberto
1 Pientka, Brigitte
1 Popescu, Andrei
1 Quirin, Kevin
1 Rabe, Florian
1 Ramos, Marcus Vinícius Midena
1 Rieu-Helft, Raphaël
1 Rouhling, Damien
1 Roux, Pierre
1 Sakaguchi, Kazuhiko
1 Santos Rego, Yuri
1 Savary-Belanger, Olivier
1 Scagnetto, Ivan
1 Siles, Vincent
...and 15 more Authors

Publications by Year

Citations contained in zbMATH Open

43 Publications have been cited 319 times in 272 Documents Cited by Year
Mizar in a nutshell. Zbl 1211.68369
Grabowski, Adam; Kornilowicz, Artur; Naumowicz, Adam
54
2010
An introduction to small scale reflection in Coq. Zbl 1211.68368
Gonthier, Georges; Mahboubi, Assia
36
2010
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
33
2016
Automated reasoning in higher-order logic using the TPTP THF infrastructure. Zbl 1211.68371
Sutcliffe, Geoff; Benzmüller, Christoph
28
2010
Abella: a system for reasoning about relational specifications. Zbl 1451.68315
Baelde, David; Chaudhuri, Kaustuv; Gacek, Andrew; Miller, Dale; Nadathur, Gopalan; Tiu, Alwen; Wang, Yuting
22
2014
Sets in Coq, Coq in Sets. Zbl 1211.03023
Barras, Bruno
21
2010
A new look at generalized rewriting in type theory. Zbl 1205.68364
Sozeau, Matthieu
15
2009
Theorema 2.0: computer-assisted natural-style mathematics. Zbl 1451.68319
Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, Wolfgang
11
2016
Formalization techniques for asymptotic reasoning in classical analysis. Zbl 1451.68329
Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien
9
2018
Formal proofs for nonlinear optimization. Zbl 1451.90131
Magron, Victor; Allamigeon, Xavier; Gaubert, Stéphane; Werner, Benjamin
8
2015
A constructive and formal proof of Lebesgue’s dominated convergence theorem in the interactive theorem prover Matita. Zbl 1175.68411
Sacerdoti Coen, Claudio; Tassi, Enrico
7
2008
A page in number theory. Zbl 1194.68206
Asperti, Andrea; Armentano, Cristian
5
2008
A formalization of Newman’s and Yokouchi’s lemmas in a higher-order language. Zbl 1171.68713
Galdino, André Luiz; Ayala-Rincón, Mauricio
5
2008
Formalization of the integral calculus in the PVS theorem prover. Zbl 1175.68410
Butler, Ricky Wayne
5
2009
Basic first-order model theory in Mizar. Zbl 1211.03024
Caminati, Marco Bright
5
2010
Formalizing scientifically applicable mathematics in a definitional framework. Zbl 1451.68333
Avron, Arnon; Cohen, Liron
5
2016
Computing with classical real numbers. Zbl 1194.68097
Kaliszyk, Cezary; O’Connor, Russell
4
2008
Formalizing a proof that \(e\) is transcendental. Zbl 1451.68317
Bingham, Jesse
4
2011
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
4
2016
C-language floating-point proofs layered with VST and Flocq. Zbl 1508.68032
Appel, Andrew W.; Bertot, Yves
3
2020
An introduction to programming and proving with dependent types in Coq. Zbl 1211.68367
Chlipala, Adam
3
2010
A string of pearls: proofs of Fermat’s little theorem. Zbl 1451.68320
Chan, Hing Lun; Norrish, Michael
3
2013
Initial semantics for higher-order typed syntax in Coq. Zbl 1451.68312
Ahrens, Benedikt; Zsido, Julianna
2
2011
A formal proof of Sasaki-Murao algorithm. Zbl 1451.68321
Coquand, Thierry; Mörtberg, Anders; Siles, Vincent
2
2012
A proof of Bertrand’s postulate. Zbl 1451.68331
Asperti, Andrea; Ricciotti, Wilmer
2
2012
Relative monads formalised. Zbl 1451.68330
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
2
2014
Certified Kruskal’s tree theorem. Zbl 1426.68289
Sternagel, Christian
2
2014
Innocuous double rounding of basic arithmetic operations. Zbl 1451.65061
Roux, Pierre
2
2014
Matita tutorial. Zbl 1451.68314
Asperti, Andrea; Ricciotti, Wilmer; Coen, Claudio Sacerdoti
2
2014
Proof auditing formalised mathematics. Zbl 1451.68328
Adams, Mark
2
2016
A Why3 proof of GMP algorithms. Zbl 1451.68342
Rieu-Helft, Raphaël
1
2019
A formalized proof of Dirichlet’s theorem on primes in arithmetic progression. Zbl 1205.68361
Harrison, John
1
2009
Implementation of Bourbaki’s Elements of mathematics in Coq. I: Theory of sets. Zbl 1211.68370
Grimm, José
1
2010
A formal proof of the Riesz representation theorem. Zbl 1451.68325
Narkawicz, Anthony
1
2011
An intrinsic encoding of a subset of C and its application to TLS network packet processing. Zbl 1451.68061
Affeldt, Reynald; Sakaguchi, Kazuhiko
1
2014
A formal verification of the theory of parity complexes. Zbl 1451.68336
Buckley, Mitchell
1
2015
Initiality for typed syntax and semantics. Zbl 1451.68072
Ahrens, Benedikt
1
2015
Now \(f\) is continuous (exercise!). Zbl 1451.68313
Arthan, Robin Denis
1
2016
Mathematical text processing in EA-style: a sequent aspect. Zbl 1451.03016
Lyaletski, Alexander
1
2016
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. Zbl 1451.68324
Lin, Yuhui; Grov, Gudmund; Arthan, Rob
1
2016
Lawvere-Tierney sheafification in homotopy type theory. Zbl 1454.03021
Quirin, Kevin; Tabareau, Nicolas
1
2016
Formalizing restriction categories. Zbl 1451.68338
Chapman, James; Uustalu, Tarmo; Veltri, Niccolò
1
2017
A formally proved, complete algorithm for path resolution with symbolic links. Zbl 1451.68171
Chen, Ran; Clochard, Martin; Marché, Claude
1
2017
C-language floating-point proofs layered with VST and Flocq. Zbl 1508.68032
Appel, Andrew W.; Bertot, Yves
3
2020
A Why3 proof of GMP algorithms. Zbl 1451.68342
Rieu-Helft, Raphaël
1
2019
Formalization techniques for asymptotic reasoning in classical analysis. Zbl 1451.68329
Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien
9
2018
Formalizing restriction categories. Zbl 1451.68338
Chapman, James; Uustalu, Tarmo; Veltri, Niccolò
1
2017
A formally proved, complete algorithm for path resolution with symbolic links. Zbl 1451.68171
Chen, Ran; Clochard, Martin; Marché, Claude
1
2017
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
33
2016
Theorema 2.0: computer-assisted natural-style mathematics. Zbl 1451.68319
Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, Wolfgang
11
2016
Formalizing scientifically applicable mathematics in a definitional framework. Zbl 1451.68333
Avron, Arnon; Cohen, Liron
5
2016
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
4
2016
Proof auditing formalised mathematics. Zbl 1451.68328
Adams, Mark
2
2016
Now \(f\) is continuous (exercise!). Zbl 1451.68313
Arthan, Robin Denis
1
2016
Mathematical text processing in EA-style: a sequent aspect. Zbl 1451.03016
Lyaletski, Alexander
1
2016
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. Zbl 1451.68324
Lin, Yuhui; Grov, Gudmund; Arthan, Rob
1
2016
Lawvere-Tierney sheafification in homotopy type theory. Zbl 1454.03021
Quirin, Kevin; Tabareau, Nicolas
1
2016
Formal proofs for nonlinear optimization. Zbl 1451.90131
Magron, Victor; Allamigeon, Xavier; Gaubert, Stéphane; Werner, Benjamin
8
2015
A formal verification of the theory of parity complexes. Zbl 1451.68336
Buckley, Mitchell
1
2015
Initiality for typed syntax and semantics. Zbl 1451.68072
Ahrens, Benedikt
1
2015
Abella: a system for reasoning about relational specifications. Zbl 1451.68315
Baelde, David; Chaudhuri, Kaustuv; Gacek, Andrew; Miller, Dale; Nadathur, Gopalan; Tiu, Alwen; Wang, Yuting
22
2014
Relative monads formalised. Zbl 1451.68330
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
2
2014
Certified Kruskal’s tree theorem. Zbl 1426.68289
Sternagel, Christian
2
2014
Innocuous double rounding of basic arithmetic operations. Zbl 1451.65061
Roux, Pierre
2
2014
Matita tutorial. Zbl 1451.68314
Asperti, Andrea; Ricciotti, Wilmer; Coen, Claudio Sacerdoti
2
2014
An intrinsic encoding of a subset of C and its application to TLS network packet processing. Zbl 1451.68061
Affeldt, Reynald; Sakaguchi, Kazuhiko
1
2014
A string of pearls: proofs of Fermat’s little theorem. Zbl 1451.68320
Chan, Hing Lun; Norrish, Michael
3
2013
A formal proof of Sasaki-Murao algorithm. Zbl 1451.68321
Coquand, Thierry; Mörtberg, Anders; Siles, Vincent
2
2012
A proof of Bertrand’s postulate. Zbl 1451.68331
Asperti, Andrea; Ricciotti, Wilmer
2
2012
Formalizing a proof that \(e\) is transcendental. Zbl 1451.68317
Bingham, Jesse
4
2011
Initial semantics for higher-order typed syntax in Coq. Zbl 1451.68312
Ahrens, Benedikt; Zsido, Julianna
2
2011
A formal proof of the Riesz representation theorem. Zbl 1451.68325
Narkawicz, Anthony
1
2011
Mizar in a nutshell. Zbl 1211.68369
Grabowski, Adam; Kornilowicz, Artur; Naumowicz, Adam
54
2010
An introduction to small scale reflection in Coq. Zbl 1211.68368
Gonthier, Georges; Mahboubi, Assia
36
2010
Automated reasoning in higher-order logic using the TPTP THF infrastructure. Zbl 1211.68371
Sutcliffe, Geoff; Benzmüller, Christoph
28
2010
Sets in Coq, Coq in Sets. Zbl 1211.03023
Barras, Bruno
21
2010
Basic first-order model theory in Mizar. Zbl 1211.03024
Caminati, Marco Bright
5
2010
An introduction to programming and proving with dependent types in Coq. Zbl 1211.68367
Chlipala, Adam
3
2010
Implementation of Bourbaki’s Elements of mathematics in Coq. I: Theory of sets. Zbl 1211.68370
Grimm, José
1
2010
A new look at generalized rewriting in type theory. Zbl 1205.68364
Sozeau, Matthieu
15
2009
Formalization of the integral calculus in the PVS theorem prover. Zbl 1175.68410
Butler, Ricky Wayne
5
2009
A formalized proof of Dirichlet’s theorem on primes in arithmetic progression. Zbl 1205.68361
Harrison, John
1
2009
A constructive and formal proof of Lebesgue’s dominated convergence theorem in the interactive theorem prover Matita. Zbl 1175.68411
Sacerdoti Coen, Claudio; Tassi, Enrico
7
2008
A page in number theory. Zbl 1194.68206
Asperti, Andrea; Armentano, Cristian
5
2008
A formalization of Newman’s and Yokouchi’s lemmas in a higher-order language. Zbl 1171.68713
Galdino, André Luiz; Ayala-Rincón, Mauricio
5
2008
Computing with classical real numbers. Zbl 1194.68097
Kaliszyk, Cezary; O’Connor, Russell
4
2008
all top 5

Cited by 385 Authors

23 Urban, Josef
14 Kaliszyk, Cezary
13 Benzmüller, Christoph Ewald
9 Naumowicz, Adam
8 Grabowski, Adam
8 Korniłowicz, Artur
8 Pąk, Karol
6 Asperti, Andrea
6 Jakubův, Jan
5 Affeldt, Reynald
5 Alama, Jesse
5 Avron, Arnon
5 Brown, Chad Edward
5 Jebelean, Tudor
5 Kohlhase, Michael
5 Kunčar, Ondřej
5 Norrish, Michael
5 Rabe, Florian
5 Steen, Alexander
5 Sutcliffe, Geoff
4 Ayala-Rincón, Mauricio
4 Chan, Hing-Lun
4 Cohen, Cyril
4 Drămnesc, Isabela
4 Heras, Jónathan
4 Magron, Victor
4 Melquiond, Guillaume
4 Paulson, Lawrence Charles
4 Popescu, Andrei
4 Ricciotti, Wilmer
4 Smolka, Gert
4 Vyskočil, Jiří
3 Ahrens, Benedikt
3 Aransay, Jesús
3 Blanchette, Jasmin Christian
3 Byliński, Czesław
3 Chaudhuri, Kaustuv
3 Chvalovský, Karel
3 Divasón, Jose
3 Gonthier, Georges
3 Kirst, Dominik
3 Krebbers, Robbert
3 Kühlwein, Daniel
3 Kumar, Ramana
3 Mahboubi, Assia
3 Momigliano, Alberto
3 Pientka, Brigitte
3 Reis, Giselle
3 Sacerdoti Coen, Claudio
3 Suda, Martin
3 Tassi, Enrico
3 Théry, Laurent
3 Traytel, Dmitry
3 Wenzel, Makarius
3 Zhan, Bohua
2 Allais, Guillaume
2 Anai, Hirokazu
2 Appel, Andrew W.
2 Arai, Noriko H.
2 Arthan, Rob D.
2 Bancerek, Grzegorz
2 Bertot, Yves
2 Birkedal, Lars
2 Boldo, Sylvie
2 Caminati, Marco Bright
2 Chapman, James T. E.
2 Chen, Ran
2 Cohen, Liron
2 Coquand, Thierry
2 Cruanes, Simon
2 Czajka, Łukasz
2 Dagand, Pierre-Evariste
2 Dénès, Maxime
2 Doczkal, Christian
2 Dufourd, Jean-François
2 Färber, Michael
2 Fukasaku, Ryoya
2 Fürer, Basil
2 Galdino, André Luiz
2 Garrigue, Jacques
2 Gauthier, Thibault
2 Grov, Gudmund
2 Heskes, Tom M.
2 Hirschowitz, André
2 Horne, Ross
2 Iwane, Hidenao
2 Janota, Mikoláš
2 Jourdan, Jacques-Henri
2 Kahl, Wolfram
2 Kobayashi, Munehiro
2 Komendantskaya, Ekaterina
2 Koutsoukou-Argyraki, Angeliki
2 Kudo, Jumma
2 Lafont, Ambroise
2 Levi, Nissan
2 Libal, Tomer
2 Lochbihler, Andreas
2 Maletzky, Alexander
2 Martin-Dorel, Érik
2 Matsuzaki, Takuya
...and 285 more Authors

Citations by Year