Commit 95cbabfb authored by Benoit Viguier's avatar Benoit Viguier
Browse files

improve parser

parent fde38521
...@@ -217,7 +217,7 @@ def generate_entry(block): ...@@ -217,7 +217,7 @@ def generate_entry(block):
# mandatory blocks: # mandatory blocks:
for i,t in {0: 'mandatory', 1: 'optional'}.items(): for i,t in {0: 'mandatory', 1: 'optional'}.items():
diagnostic(DarkGray('{}---------------------------'.format(t.ljust(9,'-')))) diagnostic(DarkGray('{}---------------------------'.format(t.ljust(9,'-'))))
if len(BIBTEX[kind][i]) > 0: if len(BIBTEX[kind][i]) > 0 and i > 0:
output += '\n' output += '\n'
for s in BIBTEX[kind][i]: for s in BIBTEX[kind][i]:
idx = find_section_index(block['sections'], s) idx = find_section_index(block['sections'], s)
......
...@@ -2,7 +2,6 @@ ...@@ -2,7 +2,6 @@
@STRING{SV = {Springer}} @STRING{SV = {Springer}}
@article{1969-Hoare, @article{1969-Hoare,
author = {C. A. R. Hoare}, author = {C. A. R. Hoare},
title = {An Axiomatic Basis for Computer Programming}, title = {An Axiomatic Basis for Computer Programming},
journal = {Commun. ACM}, journal = {Commun. ACM},
...@@ -24,7 +23,6 @@ ...@@ -24,7 +23,6 @@
} }
@article{2007-Blazy-C-chronique, @article{2007-Blazy-C-chronique,
author = {Sandrine Blazy}, author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?}, title = {Comment gagner confiance en {C} ?},
journal = {Technique et Science Informatiques}, journal = {Technique et Science Informatiques},
...@@ -40,7 +38,6 @@ ...@@ -40,7 +38,6 @@
} }
@inproceedings{2012-Appel, @inproceedings{2012-Appel,
author = {Andrew W. Appel}, author = {Andrew W. Appel},
title = {Verified Software Toolchain}, title = {Verified Software Toolchain},
booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings}, booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings},
...@@ -58,7 +55,6 @@ ...@@ -58,7 +55,6 @@
} }
@article{2015-Appel, @article{2015-Appel,
author = {Andrew W. Appel}, author = {Andrew W. Appel},
title = {Verification of a Cryptographic Primitive: SHA-256}, title = {Verification of a Cryptographic Primitive: SHA-256},
journal = {ACM Trans. Program. Lang. Syst.}, journal = {ACM Trans. Program. Lang. Syst.},
...@@ -81,7 +77,6 @@ ...@@ -81,7 +77,6 @@
} }
@book{Abrial:1996:BAP:236705, @book{Abrial:1996:BAP:236705,
author = {Jean-Raymond Abrial}, author = {Jean-Raymond Abrial},
title = {The B-book: Assigning Programs to Meanings}, title = {The B-book: Assigning Programs to Meanings},
publisher = {Cambridge University Press}, publisher = {Cambridge University Press},
...@@ -93,7 +88,6 @@ ...@@ -93,7 +88,6 @@
} }
@inproceedings{BGJ+15, @inproceedings{BGJ+15,
author = {Daniel J. Bernstein and author = {Daniel J. Bernstein and
Bernard van Gastel and Bernard van Gastel and
Wesley Janssen and Wesley Janssen and
...@@ -113,7 +107,6 @@ ...@@ -113,7 +107,6 @@
} }
@inproceedings{BLS12, @inproceedings{BLS12,
author = {Daniel J. Bernstein and author = {Daniel J. Bernstein and
Tanja Lange and Tanja Lange and
Peter Schwabe}, Peter Schwabe},
...@@ -130,7 +123,6 @@ ...@@ -130,7 +123,6 @@
} }
@inproceedings{Ber06, @inproceedings{Ber06,
author = {Daniel J. Bernstein}, author = {Daniel J. Bernstein},
title = {Curve25519: new {D}iffie-{H}ellman speed records}, title = {Curve25519: new {D}iffie-{H}ellman speed records},
booktitle = {Public Key Cryptography -- {PKC 2006}}, booktitle = {Public Key Cryptography -- {PKC 2006}},
...@@ -153,7 +145,6 @@ ...@@ -153,7 +145,6 @@
} }
@inproceedings{Beringer2015VerifiedCA, @inproceedings{Beringer2015VerifiedCA,
author = {Lennart Beringer and author = {Lennart Beringer and
Adam Petcher and Adam Petcher and
Katherine Q. Ye and Katherine Q. Ye and
...@@ -166,7 +157,6 @@ ...@@ -166,7 +157,6 @@
} }
@article{Blazy-Leroy-Clight-09, @article{Blazy-Leroy-Clight-09,
author = {Sandrine Blazy and author = {Sandrine Blazy and
Xavier Leroy}, Xavier Leroy},
title = {Mechanized semantics for the {Clight} subset of the {C} language}, title = {Mechanized semantics for the {Clight} subset of the {C} language},
...@@ -183,7 +173,6 @@ ...@@ -183,7 +173,6 @@
} }
@inproceedings{Chen2014VerifyingCS, @inproceedings{Chen2014VerifyingCS,
author = {Yu-Fang Chen and author = {Yu-Fang Chen and
Chang-Hong Hsu and Chang-Hong Hsu and
Hsin-Hung Lin and Hsin-Hung Lin and
...@@ -200,7 +189,6 @@ ...@@ -200,7 +189,6 @@
} }
@article{CpdtJFR, @article{CpdtJFR,
author = {Adam Chlipala}, author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in Coq}, title = {An Introduction to Programming and Proving with Dependent Types in Coq},
journal = {Journal of Formalized Reasoning}, journal = {Journal of Formalized Reasoning},
...@@ -214,7 +202,6 @@ ...@@ -214,7 +202,6 @@
} }
@inproceedings{DBLP:conf/itp/BartziaS14, @inproceedings{DBLP:conf/itp/BartziaS14,
author = {Evmorfia-Iro Bartzia and author = {Evmorfia-Iro Bartzia and
Pierre-Yves Strub}, Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant}, title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
...@@ -230,7 +217,6 @@ ...@@ -230,7 +217,6 @@
} }
@article{DBLP:journals/corr/BhargavanDFHPRR17, @article{DBLP:journals/corr/BhargavanDFHPRR17,
author = {Karthikeyan Bhargavan and author = {Karthikeyan Bhargavan and
Antoine Delignat{-}Lavaud and Antoine Delignat{-}Lavaud and
C{\'{e}}dric Fournet and C{\'{e}}dric Fournet and
...@@ -258,7 +244,6 @@ ...@@ -258,7 +244,6 @@
} }
@inproceedings{Erbsen2016SystematicSO, @inproceedings{Erbsen2016SystematicSO,
author = {Andres Erbsen and author = {Andres Erbsen and
Jason Gross and Jason Gross and
Adam Chlipala}, Adam Chlipala},
...@@ -270,7 +255,6 @@ ...@@ -270,7 +255,6 @@
} }
@inproceedings{Erbsen2017CraftingCE, @inproceedings{Erbsen2017CraftingCE,
author = {Andres Erbsen}, author = {Andres Erbsen},
title = {Crafting certified elliptic curve cryptography implementations in Coq}, title = {Crafting certified elliptic curve cryptography implementations in Coq},
booktitle = {}, booktitle = {},
...@@ -280,7 +264,6 @@ ...@@ -280,7 +264,6 @@
} }
@incollection{Howard1995-HOWTFN, @incollection{Howard1995-HOWTFN,
author = {W. A. Howard}, author = {W. A. Howard},
title = {The Formul\ae-as-Types Notion of Construction}, title = {The Formul\ae-as-Types Notion of Construction},
booktitle = {The Curry-Howard Isomorphism}, booktitle = {The Curry-Howard Isomorphism},
...@@ -292,7 +275,6 @@ ...@@ -292,7 +275,6 @@
} }
@techreport{ISO:C99, @techreport{ISO:C99,
author = {ISO}, author = {ISO},
title = {ISO C Standard 1999}, title = {ISO C Standard 1999},
institution = {}, institution = {},
...@@ -304,7 +286,6 @@ ...@@ -304,7 +286,6 @@
} }
@article{Leroy-backend, @article{Leroy-backend,
author = {Xavier Leroy}, author = {Xavier Leroy},
title = {A formally verified compiler back-end}, title = {A formally verified compiler back-end},
journal = {Journal of Automated Reasoning}, journal = {Journal of Automated Reasoning},
...@@ -321,7 +302,6 @@ ...@@ -321,7 +302,6 @@
} }
@article{Mon85, @article{Mon85,
author = {Peter L. Montgomery}, author = {Peter L. Montgomery},
title = {Modular Multiplication Without Trial Division}, title = {Modular Multiplication Without Trial Division},
journal = {Mathematics of Computation}, journal = {Mathematics of Computation},
...@@ -336,7 +316,6 @@ ...@@ -336,7 +316,6 @@
} }
@article{MontgomerySpeeding, @article{MontgomerySpeeding,
author = {Peter L. Montgomery}, author = {Peter L. Montgomery},
title = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264}, title = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264},
journal = {Mathematics of Computation - Math. Comput.}, journal = {Mathematics of Computation - Math. Comput.},
...@@ -351,7 +330,6 @@ ...@@ -351,7 +330,6 @@
} }
@inproceedings{Philipoom2018CorrectbyconstructionFF, @inproceedings{Philipoom2018CorrectbyconstructionFF,
author = {Jade Philipoom}, author = {Jade Philipoom},
title = {Correct-by-construction finite field arithmetic in Coq}, title = {Correct-by-construction finite field arithmetic in Coq},
booktitle = {}, booktitle = {},
...@@ -361,7 +339,6 @@ ...@@ -361,7 +339,6 @@
} }
@article{Reynolds02separationlogic, @article{Reynolds02separationlogic,
author = {John C. Reynolds}, author = {John C. Reynolds},
title = {Separation Logic: A Logic for Shared Mutable Data Structures}, title = {Separation Logic: A Logic for Shared Mutable Data Structures},
journal = {LICS}, journal = {LICS},
...@@ -375,7 +352,6 @@ ...@@ -375,7 +352,6 @@
} }
@article{Zinzindohoue2016AVE, @article{Zinzindohoue2016AVE,
author = {Jean Karim Zinzindohoue and author = {Jean Karim Zinzindohoue and
Evmorfia-Iro Bartzia and Evmorfia-Iro Bartzia and
Karthikeyan Bhargavan}, Karthikeyan Bhargavan},
...@@ -388,7 +364,6 @@ ...@@ -388,7 +364,6 @@
} }
@article{cao2018vst-floyd, @article{cao2018vst-floyd,
author = {Qinxiang Cao and author = {Qinxiang Cao and
Lennart Beringer and Lennart Beringer and
Samuel Gruetter and Samuel Gruetter and
...@@ -438,7 +413,6 @@ ...@@ -438,7 +413,6 @@
} }
@inproceedings{fiat-crypto, @inproceedings{fiat-crypto,
author = {Andres Erbsen and author = {Andres Erbsen and
Jade Philipoom and Jade Philipoom and
Jason Gross and Jason Gross and
...@@ -458,7 +432,6 @@ ...@@ -458,7 +432,6 @@
} }
@article{gonthier2008formal, @article{gonthier2008formal,
author = {Georges Gonthier}, author = {Georges Gonthier},
title = {Formal proof--the four-color theorem}, title = {Formal proof--the four-color theorem},
journal = {Notices of the AMS}, journal = {Notices of the AMS},
...@@ -497,7 +470,6 @@ ...@@ -497,7 +470,6 @@
} }
@inproceedings{zinzindohoue2017hacl, @inproceedings{zinzindohoue2017hacl,
author = {Jean-Karim Zinzindohou{\'e} and author = {Jean-Karim Zinzindohou{\'e} and
Karthikeyan Bhargavan and Karthikeyan Bhargavan and
Jonathan Protzenko and Jonathan Protzenko and
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment