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 Latest Issues 13 (2020) 12 (2019) 11 (2018) 10 (2017) 9, No. 2 (2016) 9, No. 1 (2016) 8, No. 2 (2015) 8, No. 1 (2015) 7, No. 2 (2014) 7, No. 1 (2014) 6, No. 1 (2013) 5, No. 1 (2012) 4, No. 1 (2011) 3, No. 2 (2010) 3, No. 1 (2010) 2, No. 1 (2009) 1, No. 1 (2008) 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 all top 5 Fields 62 Computer science (68-XX) 19 Mathematical logic and foundations (03-XX) 5 Number theory (11-XX) 5 Category theory; homological algebra (18-XX) 5 Real functions (26-XX) 4 Numerical analysis (65-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Information and communication theory, circuits (94-XX) 1 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Group theory and generalizations (20-XX) 1 Measure and integration (28-XX) 1 Functional analysis (46-XX) 1 Algebraic topology (55-XX) 1 Operations research, mathematical programming (90-XX) Publications by Year all cited Publications top 5 cited Publications 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 cited Publications top 5 cited Publications 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 all top 5 Cited in 40 Journals 64 Journal of Automated Reasoning 8 Logical Methods in Computer Science 7 Journal of Symbolic Computation 6 Journal of Functional Programming 6 Journal of Formalized Reasoning 5 MSCS. Mathematical Structures in Computer Science 5 Annals of Mathematics and Artificial Intelligence 4 Theoretical Computer Science 3 Formal Aspects of Computing 3 AI Communications 3 Mathematics in Computer Science 3 Formalized Mathematics 2 Theory and Practice of Logic Programming 2 Computer Languages, Systems & Structures 2 ACM Transactions on Computational Logic 2 Journal of Logical and Algebraic Methods in Programming 1 ACM Computing Surveys 1 Artificial Intelligence 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 The Mathematical Intelligencer 1 Journal of Philosophical Logic 1 SIAM Journal on Control and Optimization 1 Science of Computer Programming 1 Annals of Pure and Applied Logic 1 Computational Geometry 1 Numerical Algorithms 1 Mathematical Programming. Series A. Series B 1 Cybernetics and Systems Analysis 1 Experimental Mathematics 1 SIAM Journal on Scientific Computing 1 Mathematical Logic Quarterly (MLQ) 1 The Bulletin of Symbolic Logic 1 Journal of Difference Equations and Applications 1 Journal of Applied Mathematics 1 Sādhanā 1 Acta Numerica 1 Advances in Difference Equations 1 Boundary Value Problems 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Higher Structures all top 5 Cited in 32 Fields 248 Computer science (68-XX) 103 Mathematical logic and foundations (03-XX) 12 Number theory (11-XX) 10 Numerical analysis (65-XX) 7 Category theory; homological algebra (18-XX) 6 Real functions (26-XX) 5 General and overarching topics; collections (00-XX) 5 Algebraic topology (55-XX) 4 Linear and multilinear algebra; matrix theory (15-XX) 3 History and biography (01-XX) 3 Combinatorics (05-XX) 3 Field theory and polynomials (12-XX) 3 Commutative algebra (13-XX) 3 Algebraic geometry (14-XX) 3 Group theory and generalizations (20-XX) 3 Operations research, mathematical programming (90-XX) 2 Special functions (33-XX) 2 Geometry (51-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Information and communication theory, circuits (94-XX) 2 Mathematics education (97-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Associative rings and algebras (16-XX) 1 Partial differential equations (35-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Difference and functional equations (39-XX) 1 Approximations and expansions (41-XX) 1 Integral transforms, operational calculus (44-XX) 1 Integral equations (45-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Biology and other natural sciences (92-XX) 1 Systems theory; control (93-XX) Citations by Year