default search action

combined dblp search
author search
venue search
publication search

ask others

Journal of Formalized Reasoning, Volume 9

> Home > Journals > Journal of Formalized Reasoning

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

Volume 9, Number 1, 2016

Special Issue: Twenty Years of the QED Manifesto
QED 20th anniversary

- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/HarrisonUW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/HarrisonUW16
John Harrison, Josef Urban, Freek Wiedijk:
Preface: Twenty Years of the QED Manifesto. 1-2
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/Adams16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/Adams16
Mark Miles Adams:
Proof Auditing Formalised Mathematics. 3-32
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/Arthan16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/Arthan16
Robin Denis Arthan:
Now f is continuous (exercise!). 33-52
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/AvronC16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/AvronC16
Arnon Avron, Liron Cohen:
Formalizing Scientifically Applicable Mathematics in a Definitional Framework. 53-70
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/Beeson16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/Beeson16
Michael Beeson:
Mixing Computations and Proofs. 71-99
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/BlanchetteKPU16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/BlanchetteKPU16
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. 101-148
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/BuchbergerJKMW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/BuchbergerJKMW16
Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger:
Theorema 2.0: Computer-Assisted Natural-Style Mathematics. 149-185
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/Carneiro16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/Carneiro16
Mario Carneiro:
Conversion of HOL Light proofs into Metamath. 187-200
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/KohlhaseR16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/KohlhaseR16
Michael Kohlhase, Florian Rabe:
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. 201-234
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/Lyaletski16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/Lyaletski16
Alexander V. Lyaletski:
Mathematical Text Processing in EA-style: a Sequent Aspect. 235-264

Volume 9, Number 2, 2016

Articles

- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/Grimm16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/Grimm16
José Grimm:
Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. 1-52
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/RamosAMQ16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/RamosAMQ16
Marcus Vinícius Midena Ramos, José Carlos Bacelar Almeida, Nelma Moreira, Ruy José Guerra Barretto de Queiroz:
Formalization of the pumping lemma for context-free languages. 53-68
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/LinGA16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/LinGA16
Yuhui Lin, Gudmund Grov, Rob Arthan:
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. 69-130
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/QuirinT16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/QuirinT16
Kevin Quirin, Nicolas Tabareau:
Lawvere-Tierney sheafification in Homotopy Type Theory. 131-161

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.