Search dblp for Publications

export results for "stream:streams/journals/jfrea:"

 download as .bib file

@article{DBLP:journals/jfrea/AppelB20,
  author    = {Andrew W. Appel and
               Yves Bertot},
  title     = {C floating-point proofs layered with {VST} and Flocq},
  journal   = {J. Formaliz. Reason.},
  volume    = {13},
  number    = {1},
  pages     = {1--16},
  year      = {2020},
  url       = {https://doi.org/10.6092/issn.1972-5787/11442},
  doi       = {10.6092/issn.1972-5787/11442},
  timestamp = {Fri, 27 May 2022 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AppelB20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AppelB20a,
  author    = {Andrew W. Appel and
               Yves Bertot},
  title     = {Corrigendum: {C} floating-point proofs layered with {VST} and Flocq},
  journal   = {J. Formaliz. Reason.},
  volume    = {13},
  number    = {1},
  year      = {2020},
  url       = {https://doi.org/10.6092/issn.1972-5787/12643},
  doi       = {10.6092/issn.1972-5787/12643},
  timestamp = {Fri, 27 May 2022 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AppelB20a.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AlessiCGHLS19,
  author    = {Fabio Alessi and
               Alberto Ciaffaglione and
               Pietro Di Gianantonio and
               Furio Honsell and
               Marina Lenisa and
               Ivan Scagnetto},
  title     = {{LF+} in Coq for "fast and loose" reasoning},
  journal   = {J. Formaliz. Reason.},
  volume    = {12},
  number    = {1},
  pages     = {11--51},
  year      = {2019},
  url       = {https://doi.org/10.6092/issn.1972-5787/9757},
  doi       = {10.6092/issn.1972-5787/9757},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AlessiCGHLS19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/PadmanabhanZ19,
  author    = {Ranganathan Padmanabhan and
               Yang Zhang},
  title     = {Commutativity Theorems in Groups with Power-like Maps},
  journal   = {J. Formaliz. Reason.},
  volume    = {12},
  number    = {1},
  pages     = {1--10},
  year      = {2019},
  url       = {https://doi.org/10.6092/issn.1972-5787/8751},
  doi       = {10.6092/issn.1972-5787/8751},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/PadmanabhanZ19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Rieu-Helft19,
  author    = {Rapha{\"{e}}l Rieu{-}Helft},
  title     = {A Why3 proof of {GMP} algorithms},
  journal   = {J. Formaliz. Reason.},
  volume    = {12},
  number    = {1},
  pages     = {53--97},
  year      = {2019},
  url       = {https://doi.org/10.6092/issn.1972-5787/9730},
  doi       = {10.6092/issn.1972-5787/9730},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Rieu-Helft19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AffeldtCR18,
  author    = {Reynald Affeldt and
               Cyril Cohen and
               Damien Rouhling},
  title     = {Formalization Techniques for Asymptotic Reasoning in Classical Analysis},
  journal   = {J. Formaliz. Reason.},
  volume    = {11},
  number    = {1},
  pages     = {43--76},
  year      = {2018},
  url       = {https://doi.org/10.6092/issn.1972-5787/8124},
  doi       = {10.6092/issn.1972-5787/8124},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AffeldtCR18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Lescanne18,
  author    = {Pierre Lescanne},
  title     = {Dependent Types for Extensive Games},
  journal   = {J. Formaliz. Reason.},
  volume    = {11},
  number    = {1},
  pages     = {1--17},
  year      = {2018},
  url       = {https://doi.org/10.6092/issn.1972-5787/7517},
  doi       = {10.6092/issn.1972-5787/7517},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Lescanne18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/MunozND18,
  author    = {C{\'{e}}sar A. Mu{\~{n}}oz and
               Anthony J. Narkawicz and
               Aaron Dutle},
  title     = {A Decision Procedure for Univariate Polynomial Systems Based on Root
               Counting and Interval Subdivision},
  journal   = {J. Formaliz. Reason.},
  volume    = {11},
  number    = {1},
  pages     = {19--41},
  year      = {2018},
  url       = {https://doi.org/10.6092/issn.1972-5787/8212},
  doi       = {10.6092/issn.1972-5787/8212},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/MunozND18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BagnallMS17,
  author    = {Alexander Bagnall and
               Samuel Merten and
               Gordon Stewart},
  title     = {A Library for Algorithmic Game Theory in Ssreflect/Coq},
  journal   = {J. Formaliz. Reason.},
  volume    = {10},
  number    = {1},
  pages     = {67--95},
  year      = {2017},
  url       = {https://doi.org/10.6092/issn.1972-5787/7235},
  doi       = {10.6092/issn.1972-5787/7235},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/BagnallMS17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/ChapmanUV17,
  author    = {James Chapman and
               Tarmo Uustalu and
               Niccol{\`{o}} Veltri},
  title     = {Formalizing Restriction Categories},
  journal   = {J. Formaliz. Reason.},
  volume    = {10},
  number    = {1},
  pages     = {1--36},
  year      = {2017},
  url       = {https://doi.org/10.6092/issn.1972-5787/6237},
  doi       = {10.6092/issn.1972-5787/6237},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/ChapmanUV17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/ChenCM17,
  author    = {Ran Chen and
               Martin Clochard and
               Claude March{\'{e}}},
  title     = {A Formally Proved, Complete Algorithm for Path Resolution with Symbolic
               Links},
  journal   = {J. Formaliz. Reason.},
  volume    = {10},
  number    = {1},
  pages     = {51--66},
  year      = {2017},
  url       = {https://doi.org/10.6092/issn.1972-5787/6767},
  doi       = {10.6092/issn.1972-5787/6767},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/ChenCM17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Rauglaudre17,
  author    = {Daniel de Rauglaudre},
  title     = {Formal Proof of Banach-Tarski Paradox},
  journal   = {J. Formaliz. Reason.},
  volume    = {10},
  number    = {1},
  pages     = {37--49},
  year      = {2017},
  url       = {https://doi.org/10.6092/issn.1972-5787/6927},
  doi       = {10.6092/issn.1972-5787/6927},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Rauglaudre17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Adams16,
  author    = {Mark Miles Adams},
  title     = {Proof Auditing Formalised Mathematics},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {3--32},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4576},
  doi       = {10.6092/issn.1972-5787/4576},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Adams16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Arthan16,
  author    = {Robin Denis Arthan},
  title     = {Now f is continuous (exercise!)},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {33--52},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4566},
  doi       = {10.6092/issn.1972-5787/4566},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Arthan16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AvronC16,
  author    = {Arnon Avron and
               Liron Cohen},
  title     = {Formalizing Scientifically Applicable Mathematics in a Definitional
               Framework},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {53--70},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4573},
  doi       = {10.6092/issn.1972-5787/4573},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AvronC16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Beeson16,
  author    = {Michael Beeson},
  title     = {Mixing Computations and Proofs},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {71--99},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4552},
  doi       = {10.6092/issn.1972-5787/4552},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Beeson16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BlanchetteKPU16,
  author    = {Jasmin Christian Blanchette and
               Cezary Kaliszyk and
               Lawrence C. Paulson and
               Josef Urban},
  title     = {Hammering towards {QED}},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {101--148},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4593},
  doi       = {10.6092/issn.1972-5787/4593},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/BlanchetteKPU16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BuchbergerJKMW16,
  author    = {Bruno Buchberger and
               Tudor Jebelean and
               Temur Kutsia and
               Alexander Maletzky and
               Wolfgang Windsteiger},
  title     = {Theorema 2.0: Computer-Assisted Natural-Style Mathematics},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {149--185},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4568},
  doi       = {10.6092/issn.1972-5787/4568},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/BuchbergerJKMW16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Carneiro16,
  author    = {Mario Carneiro},
  title     = {Conversion of {HOL} Light proofs into Metamath},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {187--200},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4596},
  doi       = {10.6092/issn.1972-5787/4596},
  timestamp = {Thu, 25 Nov 2021 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/journals/jfrea/Carneiro16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Grimm16,
  author    = {Jos{\'{e}} Grimm},
  title     = {Implementation of Bourbaki's Elements of Mathematics in Coq: Part
               Two, From Natural Numbers to Real Numbers},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {2},
  pages     = {1--52},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4771},
  doi       = {10.6092/issn.1972-5787/4771},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Grimm16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/HarrisonUW16,
  author    = {John Harrison and
               Josef Urban and
               Freek Wiedijk},
  title     = {Preface: Twenty Years of the {QED} Manifesto},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {1--2},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/5974},
  doi       = {10.6092/issn.1972-5787/5974},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/HarrisonUW16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/KohlhaseR16,
  author    = {Michael Kohlhase and
               Florian Rabe},
  title     = {{QED} Reloaded: Towards a Pluralistic Formal Library of Mathematical
               Knowledge},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {201--234},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4570},
  doi       = {10.6092/issn.1972-5787/4570},
  timestamp = {Fri, 20 Nov 2020 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/journals/jfrea/KohlhaseR16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/LinGA16,
  author    = {Yuhui Lin and
               Gudmund Grov and
               Rob Arthan},
  title     = {Understanding and maintaining tactics graphically {OR} how we are
               learning that a diagram can be worth more than 10K LoC},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {2},
  pages     = {69--130},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/6298},
  doi       = {10.6092/issn.1972-5787/6298},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/LinGA16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Lyaletski16,
  author    = {Alexander V. Lyaletski},
  title     = {Mathematical Text Processing in EA-style: a Sequent Aspect},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {1},
  pages     = {235--264},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/4569},
  doi       = {10.6092/issn.1972-5787/4569},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Lyaletski16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/QuirinT16,
  author    = {Kevin Quirin and
               Nicolas Tabareau},
  title     = {Lawvere-Tierney sheafification in Homotopy Type Theory},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {2},
  pages     = {131--161},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/6232},
  doi       = {10.6092/issn.1972-5787/6232},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/QuirinT16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/RamosAMQ16,
  author    = {Marcus Vin{\'{\i}}cius Midena Ramos and
               Jos{\'{e}} Carlos Bacelar Almeida and
               Nelma Moreira and
               Ruy Jos{\'{e}} Guerra Barretto de Queiroz},
  title     = {Formalization of the pumping lemma for context-free languages},
  journal   = {J. Formaliz. Reason.},
  volume    = {9},
  number    = {2},
  pages     = {53--68},
  year      = {2016},
  url       = {https://doi.org/10.6092/issn.1972-5787/5595},
  doi       = {10.6092/issn.1972-5787/5595},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/RamosAMQ16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Ahrens15,
  author    = {Benedikt Ahrens},
  title     = {Initiality for Typed Syntax and Semantics},
  journal   = {J. Formaliz. Reason.},
  volume    = {8},
  number    = {2},
  pages     = {1--155},
  year      = {2015},
  url       = {https://doi.org/10.6092/issn.1972-5787/4712},
  doi       = {10.6092/issn.1972-5787/4712},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Ahrens15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BelangerMP15,
  author    = {Olivier Savary B{\'{e}}langer and
               Stefan Monnier and
               Brigitte Pientka},
  title     = {Programming type-safe transformations using higher-order abstract
               syntax},
  journal   = {J. Formaliz. Reason.},
  volume    = {8},
  number    = {1},
  pages     = {49--91},
  year      = {2015},
  url       = {https://doi.org/10.6092/issn.1972-5787/5122},
  doi       = {10.6092/issn.1972-5787/5122},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/BelangerMP15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Buckley15,
  author    = {Mitchell Buckley},
  title     = {A formal verification of the theory of parity complexes},
  journal   = {J. Formaliz. Reason.},
  volume    = {8},
  number    = {1},
  pages     = {25--48},
  year      = {2015},
  url       = {https://doi.org/10.6092/issn.1972-5787/5010},
  doi       = {10.6092/issn.1972-5787/5010},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Buckley15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Guidi15,
  author    = {Ferruccio Guidi},
  title     = {Verified Representations of Landau's "Grundlagen" in the lambda-delta
               Family and in the Calculus of Constructions},
  journal   = {J. Formaliz. Reason.},
  volume    = {8},
  number    = {1},
  pages     = {93--116},
  year      = {2015},
  url       = {https://doi.org/10.6092/issn.1972-5787/4716},
  doi       = {10.6092/issn.1972-5787/4716},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Guidi15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/MagronAGW15,
  author    = {Victor Magron and
               Xavier Allamigeon and
               St{\'{e}}phane Gaubert and
               Benjamin Werner},
  title     = {Formal Proofs for Nonlinear Optimization},
  journal   = {J. Formaliz. Reason.},
  volume    = {8},
  number    = {1},
  pages     = {1--24},
  year      = {2015},
  url       = {https://doi.org/10.6092/issn.1972-5787/4319},
  doi       = {10.6092/issn.1972-5787/4319},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/MagronAGW15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AffeldtS14,
  author    = {Reynald Affeldt and
               Kazuhiko Sakaguchi},
  title     = {An Intrinsic Encoding of a Subset of {C} and its Application to {TLS}
               Network Packet Processing},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {1},
  pages     = {63--104},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4317},
  doi       = {10.6092/issn.1972-5787/4317},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AffeldtS14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AltenkirchCU14,
  author    = {Thorsten Altenkirch and
               James Chapman and
               Tarmo Uustalu},
  title     = {Relative Monads Formalised},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {1},
  pages     = {1--43},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4389},
  doi       = {10.6092/issn.1972-5787/4389},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AltenkirchCU14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AspertiRC14,
  author    = {Andrea Asperti and
               Wilmer Ricciotti and
               Claudio Sacerdoti Coen},
  title     = {Matita Tutorial},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {2},
  pages     = {91--199},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4651},
  doi       = {10.6092/issn.1972-5787/4651},
  timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AspertiRC14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BaeldeCGMNTW14,
  author    = {David Baelde and
               Kaustuv Chaudhuri and
               Andrew Gacek and
               Dale Miller and
               Gopalan Nadathur and
               Alwen Tiu and
               Yuting Wang},
  title     = {Abella: {A} System for Reasoning about Relational Specifications},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {2},
  pages     = {1--89},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4650},
  doi       = {10.6092/issn.1972-5787/4650},
  timestamp = {Sun, 25 Jul 2021 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/BaeldeCGMNTW14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BertotA14,
  author    = {Yves Bertot and
               Guillaume Allais},
  title     = {Views of {PI:} Definition and computation},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {1},
  pages     = {105--129},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4343},
  doi       = {10.6092/issn.1972-5787/4343},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/BertotA14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Roux14,
  author    = {Pierre Roux},
  title     = {Innocuous Double Rounding of Basic Arithmetic Operations},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {1},
  pages     = {131--142},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4359},
  doi       = {10.6092/issn.1972-5787/4359},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Roux14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Sternagel14,
  author    = {Christian Sternagel},
  title     = {Certified Kruskal's Tree Theorem},
  journal   = {J. Formaliz. Reason.},
  volume    = {7},
  number    = {1},
  pages     = {45--62},
  year      = {2014},
  url       = {https://doi.org/10.6092/issn.1972-5787/4213},
  doi       = {10.6092/issn.1972-5787/4213},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Sternagel14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/0001HN13,
  author    = {Andrei Popescu and
               Johannes H{\"{o}}lzl and
               Tobias Nipkow},
  title     = {Formal Verification of Language-Based Concurrent Noninterference},
  journal   = {J. Formaliz. Reason.},
  volume    = {6},
  number    = {1},
  pages     = {1--30},
  year      = {2013},
  url       = {https://doi.org/10.6092/issn.1972-5787/3690},
  doi       = {10.6092/issn.1972-5787/3690},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/0001HN13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Ayala-RinconR13,
  author    = {Mauricio Ayala{-}Rinc{\'{o}}n and
               Yuri Santos Rego},
  title     = {Formalization in {PVS} of Balancing Properties Necessary for Proving
               Security of the Dolev-Yao Cascade Protocol Model},
  journal   = {J. Formaliz. Reason.},
  volume    = {6},
  number    = {1},
  pages     = {31--61},
  year      = {2013},
  url       = {https://doi.org/10.6092/issn.1972-5787/3720},
  doi       = {10.6092/issn.1972-5787/3720},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Ayala-RinconR13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/ChanN13,
  author    = {Hing{-}Lun Chan and
               Michael Norrish},
  title     = {A String of Pearls: Proofs of Fermat's Little Theorem},
  journal   = {J. Formaliz. Reason.},
  volume    = {6},
  number    = {1},
  pages     = {63--87},
  year      = {2013},
  url       = {https://doi.org/10.6092/issn.1972-5787/3728},
  doi       = {10.6092/issn.1972-5787/3728},
  timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/journals/jfrea/ChanN13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Neron13,
  author    = {Pierre Neron},
  title     = {A Formal Proof of Square Root and Division Elimination in Embedded
               Programs},
  journal   = {J. Formaliz. Reason.},
  volume    = {6},
  number    = {1},
  pages     = {89--111},
  year      = {2013},
  url       = {https://doi.org/10.6092/issn.1972-5787/3887},
  doi       = {10.6092/issn.1972-5787/3887},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Neron13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AspertiR12,
  author    = {Andrea Asperti and
               Wilmer Ricciotti},
  title     = {A proof of Bertrand's postulate},
  journal   = {J. Formaliz. Reason.},
  volume    = {5},
  number    = {1},
  pages     = {37--57},
  year      = {2012},
  url       = {https://doi.org/10.6092/issn.1972-5787/3406},
  doi       = {10.6092/issn.1972-5787/3406},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AspertiR12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/CoquandMS12,
  author    = {Thierry Coquand and
               Anders M{\"{o}}rtberg and
               Vincent Siles},
  title     = {A formal proof of Sasaki-Murao algorithm},
  journal   = {J. Formaliz. Reason.},
  volume    = {5},
  number    = {1},
  pages     = {27--36},
  year      = {2012},
  url       = {https://doi.org/10.6092/issn.1972-5787/2615},
  doi       = {10.6092/issn.1972-5787/2615},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/CoquandMS12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Guidi12,
  author    = {Ferruccio Guidi},
  title     = {Standardization and Confluence in Pure Lambda-Calculus Formalized
               for the Matita Theorem Prover},
  journal   = {J. Formaliz. Reason.},
  volume    = {5},
  number    = {1},
  pages     = {1--25},
  year      = {2012},
  url       = {https://doi.org/10.6092/issn.1972-5787/3392},
  doi       = {10.6092/issn.1972-5787/3392},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Guidi12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AhrensZ11,
  author    = {Benedikt Ahrens and
               Julianna Zsido},
  title     = {Initial Semantics for higher-order typed syntax in Coq},
  journal   = {J. Formaliz. Reason.},
  volume    = {4},
  number    = {1},
  pages     = {25--69},
  year      = {2011},
  url       = {https://doi.org/10.6092/issn.1972-5787/2066},
  doi       = {10.6092/issn.1972-5787/2066},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AhrensZ11.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Bingham11,
  author    = {Jesse Bingham},
  title     = {Formalizing a Proof that e is Transcendental},
  journal   = {J. Formaliz. Reason.},
  volume    = {4},
  number    = {1},
  pages     = {71--84},
  year      = {2011},
  url       = {https://doi.org/10.6092/issn.1972-5787/2269},
  doi       = {10.6092/issn.1972-5787/2269},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Bingham11.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/ChiarabiniD11,
  author    = {Luca Chiarabini and
               Olivier Danvy},
  title     = {A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration},
  journal   = {J. Formaliz. Reason.},
  volume    = {4},
  number    = {1},
  pages     = {85--109},
  year      = {2011},
  url       = {https://doi.org/10.6092/issn.1972-5787/2225},
  doi       = {10.6092/issn.1972-5787/2225},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/ChiarabiniD11.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Narkawicz11,
  author    = {Anthony Narkawicz},
  title     = {A Formal Proof Of The Riesz Representation Theorem},
  journal   = {J. Formaliz. Reason.},
  volume    = {4},
  number    = {1},
  pages     = {1--24},
  year      = {2011},
  url       = {https://doi.org/10.6092/issn.1972-5787/1952},
  doi       = {10.6092/issn.1972-5787/1952},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Narkawicz11.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Barras10,
  author    = {Bruno Barras},
  title     = {Sets in Coq, Coq in Sets},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {1},
  pages     = {29--48},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1695},
  doi       = {10.6092/issn.1972-5787/1695},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Barras10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Caminati10,
  author    = {Marco B. Caminati},
  title     = {Basic first-order model theory in Mizar},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {1},
  pages     = {49--77},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1974},
  doi       = {10.6092/issn.1972-5787/1974},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Caminati10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Chlipala10,
  author    = {Adam Chlipala},
  title     = {An Introduction to Programming and Proving with Dependent Types in
               Coq},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {2},
  pages     = {1--93},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1978},
  doi       = {10.6092/issn.1972-5787/1978},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Chlipala10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/GonthierM10,
  author    = {Georges Gonthier and
               Assia Mahboubi},
  title     = {An introduction to small scale reflection in Coq},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {2},
  pages     = {95--152},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1979},
  doi       = {10.6092/issn.1972-5787/1979},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/GonthierM10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/GrabowskiKN10,
  author    = {Adam Grabowski and
               Artur Kornilowicz and
               Adam Naumowicz},
  title     = {Mizar in a Nutshell},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {2},
  pages     = {153--245},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1980},
  doi       = {10.6092/issn.1972-5787/1980},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/GrabowskiKN10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Grimm10,
  author    = {Jos{\'{e}} Grimm},
  title     = {Implementation of Bourbaki's Elements of Mathematics in Coq: Part
               One, Theory of Sets},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {1},
  pages     = {79--126},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1899},
  doi       = {10.6092/issn.1972-5787/1899},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Grimm10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/SutcliffeB10,
  author    = {Geoff Sutcliffe and
               Christoph Benzm{\"{u}}ller},
  title     = {Automated Reasoning in Higher-Order Logic using the {TPTP} {THF} Infrastructure},
  journal   = {J. Formaliz. Reason.},
  volume    = {3},
  number    = {1},
  pages     = {1--27},
  year      = {2010},
  url       = {https://doi.org/10.6092/issn.1972-5787/1710},
  doi       = {10.6092/issn.1972-5787/1710},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/SutcliffeB10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Butler09,
  author    = {Ricky W. Butler},
  title     = {Formalization of the Integral Calculus in the {PVS} Theorem Prover},
  journal   = {J. Formaliz. Reason.},
  volume    = {2},
  number    = {1},
  pages     = {1--26},
  year      = {2009},
  url       = {https://doi.org/10.6092/issn.1972-5787/1349},
  doi       = {10.6092/issn.1972-5787/1349},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Butler09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Harrison09,
  author    = {John Harrison},
  title     = {A formalized proof of Dirichlet's theorem on primes in arithmetic
               progression},
  journal   = {J. Formaliz. Reason.},
  volume    = {2},
  number    = {1},
  pages     = {63--83},
  year      = {2009},
  url       = {https://doi.org/10.6092/issn.1972-5787/1558},
  doi       = {10.6092/issn.1972-5787/1558},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Harrison09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/KaliszykO09,
  author    = {Cezary Kaliszyk and
               Russell O'Connor},
  title     = {Computing with Classical Real Numbers},
  journal   = {J. Formaliz. Reason.},
  volume    = {2},
  number    = {1},
  pages     = {27--39},
  year      = {2009},
  url       = {https://doi.org/10.6092/issn.1972-5787/1411},
  doi       = {10.6092/issn.1972-5787/1411},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/KaliszykO09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/Sozeau09,
  author    = {Matthieu Sozeau},
  title     = {A New Look at Generalized Rewriting in Type Theory},
  journal   = {J. Formaliz. Reason.},
  volume    = {2},
  number    = {1},
  pages     = {41--62},
  year      = {2009},
  url       = {https://doi.org/10.6092/issn.1972-5787/1574},
  doi       = {10.6092/issn.1972-5787/1574},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/Sozeau09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AspertiA08,
  author    = {Andrea Asperti and
               Cristian Armentano},
  title     = {A Page in Number Theory},
  journal   = {J. Formaliz. Reason.},
  volume    = {1},
  number    = {1},
  pages     = {1--23},
  year      = {2008},
  url       = {https://doi.org/10.6092/issn.1972-5787/385},
  doi       = {10.6092/issn.1972-5787/385},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/AspertiA08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/CoenT08,
  author    = {Claudio Sacerdoti Coen and
               Enrico Tassi},
  title     = {A constructive and formal proof of Lebesgue's Dominated Convergence
               Theorem in the interactive theorem prover Matita},
  journal   = {J. Formaliz. Reason.},
  volume    = {1},
  number    = {1},
  pages     = {51--89},
  year      = {2008},
  url       = {https://doi.org/10.6092/issn.1972-5787/1334},
  doi       = {10.6092/issn.1972-5787/1334},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/CoenT08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/GaldinoA08,
  author    = {Andr{\'{e}} Luiz Galdino and
               Mauricio Ayala{-}Rinc{\'{o}}n},
  title     = {A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order
               Language},
  journal   = {J. Formaliz. Reason.},
  volume    = {1},
  number    = {1},
  pages     = {39--50},
  year      = {2008},
  url       = {https://doi.org/10.6092/issn.1972-5787/1347},
  doi       = {10.6092/issn.1972-5787/1347},
  timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/GaldinoA08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/VidalADMP08,
  author    = {Concepci{\'{o}}n Vidal and
               Felicidad Aguado and
               Jos{\'{e}} Luis Doncel and
               Jos{\'{e}} Mar{\'{\i}}a Molinelli and
               Gilberto P{\'{e}}rez},
  title     = {Genetic Algorithms in Coq: Generalization and Formalization of the
               crossover operator},
  journal   = {J. Formaliz. Reason.},
  volume    = {1},
  number    = {1},
  pages     = {25--37},
  year      = {2008},
  url       = {https://doi.org/10.6092/issn.1972-5787/1052},
  doi       = {10.6092/issn.1972-5787/1052},
  timestamp = {Thu, 16 Jun 2022 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/jfrea/VidalADMP08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics