default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp for Publications
export results for "stream: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 = {Sat, 30 Sep 2023 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 = {Sun, 06 Oct 2024 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 = {Sun, 02 Oct 2022 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 = {Mon, 26 Jun 2023 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, 06 Oct 2024 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 = {Sat, 30 Sep 2023 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 = {Fri, 23 Aug 2024 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}
}
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
retrieved on 2024-11-10 05:34 CET from data curated by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
