@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -ob select2015.bib -c 'lixequipe : "Parsifal"' -c year=2015 master.bib}}
@misc{Bedwyr,
key = {Bedwyr},
title = {The {B}edwyr system},
note = {Available at
\url{http://slimmer.gforge.inria.fr/bedwyr/}},
year = {2015},
lixequipe = {Parsifal},
lixcategorie = {SW}
}
@inproceedings{accattoli15aplas,
title = {{A Strong Distillery}},
author = {Beniamino Accattoli and Pablo Barenbaum and Damiano
Mazza},
booktitle = {{Programming Languages and Systems - 13th Asian
Symposium, APLAS 2015}},
address = {Pohang, South Korea},
series = {Lecture notes in computer science},
volume = {9458},
pages = {231--250},
year = {2015},
month = nov,
doi = {10.1007/978-3-319-26529-2\_13},
url = {https://hal.archives-ouvertes.fr/hal-01244838},
pdf = {https://hal.archives-ouvertes.fr/hal-01244838/document},
hal_id = {hal-01244838},
hal_version = {v1},
x-proceedings = {yes},
x-international-audience = {yes},
x-editorial-board = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no},
lixequipe = {Parsifal},
lixcategorie = {CIA}
}
@inproceedings{accattoli15lics,
title = {{On the Relative Usefulness of Fireballs}},
author = {Beniamino Accattoli and Claudio Sacerdoti Coen},
booktitle = {{30th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2015}},
address = {Kyoto, Japan},
year = {2015},
month = jul,
doi = {10.1109/LICS.2015.23},
url = {https://hal.archives-ouvertes.fr/hal-01244833},
pdf = {https://hal.archives-ouvertes.fr/hal-01244833/document},
hal_id = {hal-01244833},
hal_version = {v1},
x-proceedings = {yes},
x-international-audience = {yes},
x-editorial-board = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no},
lixequipe = {Parsifal},
lixcategorie = {CIA}
}
@article{accattoli15tcs,
title = {{Proof nets and the call-by-value λ-calculus}},
author = {Beniamino Accattoli},
journal = {{Journal of Theoretical Computer Science (TCS)}},
publisher = {{Elsevier}},
year = {2015},
doi = {10.1016/j.tcs.2015.08.006},
url = {https://hal.archives-ouvertes.fr/hal-01244842},
pdf = {https://hal.archives-ouvertes.fr/hal-01244842/document},
hal_id = {hal-01244842},
hal_version = {v1},
x-international-audience = {yes},
x-editorial-board = {yes},
x-scientific-popularization = {no},
lixequipe = {Parsifal},
lixcategorie = {RI}
}
@inproceedings{baaz15lics,
author = {Matthias Baaz and Alexander Leitsch and Giselle Reis},
title = {A Note on the Complexity of Classical and
Intuitionistic Proofs},
booktitle = {30th Annual {ACM/IEEE} Symposium on Logic in Computer
Science, {LICS} 2015, Kyoto, Japan, July 6-10, 2015},
pages = {657--666},
year = {2015},
url = {http://dx.doi.org/10.1109/LICS.2015.66},
doi = {10.1109/LICS.2015.66},
lixequipe = {Parsifal},
lixcategorie = {CIA},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {parsifal EXT},
x-type = {article},
x-support = {actes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{blanco15wof,
author = {Roberto Blanco and Dale Miller},
title = {Proof Outlines as Proof Certificates: a system
description},
year = {2015},
url = {http://www.eprover.org/EVENTS/IWIL-2015.html},
month = nov,
editor = {Iliano Cervesato and Carsten Sch{\"u}rmann},
booktitle = {Proceedings First International Workshop on Focusing},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {197},
publisher = {Open Publishing Association},
pages = {7--14},
doi = {10.4204/EPTCS.197.2},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{brocknannestad15linearity,
author = {Taus Brock{-}Nannestad and Nicolas Guenot},
title = {Cut Elimination in Multifocused Linear Logic},
booktitle = {Proceedings Third International Workshop on Linearity,
{LINEARITY} 2014, Vienna, Austria, 13th July, 2014.},
pages = {24--33},
year = {2015},
editor = {Sandra Alves and Iliano Cervesato},
series = {{EPTCS}},
volume = {176},
url = {http://dx.doi.org/10.4204/EPTCS.176.3},
doi = {10.4204/EPTCS.176.3},
lixcategorie = {RI},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{brocknannestad15mfps,
author = {Taus Brock{-}Nannestad and Nicolas Guenot},
title = {Focused Linear Logic and the $\lambda$-calculus},
booktitle = {Proceedings of the Thirty-first Conference on the
Mathematical Foundations of Programming Semantics,
Nijmegen, The Netherlands, June 22--25, 2015},
pages = {314--329},
year = {2015},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-pays = {NL},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{brocknannestad15ppdp,
author = {Taus Brock{-}Nannestad and Nicolas Guenot and Daniel
Gustafsson},
title = {Computation in focused intuitionistic logic},
booktitle = {Proceedings of the 17th International Symposium on
Principles and Practice of Declarative Programming,
Siena, Italy, July 14--16, 2015},
pages = {43--54},
year = {2015},
editor = {Moreno Falaschi and Elvira Albert},
url = {http://doi.acm.org/10.1145/2790449.2790528},
doi = {10.1145/2790449.2790528},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes}
}
@inproceedings{brocknannestad15tableaux,
author = {Taus Brock-Nannestad and Kaustuv Chaudhuri},
title = {Disproving Using the Inverse Method by Iterated
Refinement of Finite Approximations},
booktitle = {Proceedings of the 24th Automated Reasoning with
Analytic Tableaux and Related Methods (TABLEAUX)},
year = {2015},
editor = {Hans de Nivelle},
volume = {9323},
series = {LNAI},
month = sep,
pages = {153--168},
address = {Wroc{\l}aw, Poland},
publisher = {Springer},
doi = {10.1007/978-3-319-24312-2\_11},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
lixcategorie = {CIA},
lixequipe = {Parsifal},
url = {http://chaudhuri.info/papers/draft15saturate.pdf}
}
@inproceedings{chaudhuri15cpp,
author = {Kaustuv Chaudhuri and Matteo Cimini and Dale Miller},
title = {A Lightweight Formalization of the Metatheory of
Bisimulation-Up-To},
booktitle = {Proceedings of the 4th ACM-SIGPLAN Conference on
Certified Programs and Proofs},
doi = {10.1145/2676724.2693170},
year = {2015},
editor = {Xavier Leroy and Alwen Tiu},
pages = {157--166},
month = jan,
address = {Mumbai, India},
publisher = {ACM},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {US},
url = {https://hal.inria.fr/hal-01091524/document}
}
@inproceedings{chaudhuri15lpar,
author = {Kaustuv Chaudhuri and Giselle Reis},
title = {An adequate compositional encoding of bigraph
structure in linear logic with subexponentials.},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR)},
year = {2015},
editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver
and Andrei Voronkov},
month = nov,
publisher = {Springer},
series = {LNCS},
volume = {9450},
pages = {146--161},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
url = {http://chaudhuri.info/papers/lpar15bigraphs.pdf},
doi = {10.1007/978-3-662-48899-7\_11},
x-id-hal = {hal-01208362}
}
@phdthesis{chihani15phd,
author = {Zakaria Chihani},
title = {Certification of First-order proofs in classical and
intuitionistic logics},
school = {Ecole Polytechnique},
year = {2015},
month = aug,
lixcategorie = {TH},
lixequipe = {Parsifal}
}
@inproceedings{heath15pxtp,
author = {Quentin Heath and Dale Miller},
title = {A framework for proof certificates in finite state
exploration},
booktitle = {Proceedings of the Fourth Workshop on Proof eXchange
for Theorem Proving},
year = {2015},
editor = {Cezary Kaliszyk and Andrei Paskevich},
number = {186},
series = {Electronic Proceedings in Theoretical Computer
Science},
pages = {11--26},
month = aug,
publisher = {Open Publishing Association},
doi = {10.4204/EPTCS.186.4},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pxtp2015.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {CADE},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{leitsch15epsilon,
author = {Alexander Leitsch and Giselle Reis and Bruno
Woltzenlogel Paleo},
title = {Epsilon Terms in Intuitionistic Sequent Calculus},
year = {2015},
note = {Hilbert's Epsilon and Tau in Logic, Informatics and
Linguistics Workshop},
lixequipe = {Parsifal},
lixcategorie = {CIA}
}
@inproceedings{liang15lpar,
author = {Chuck Liang and Dale Miller},
title = {On Subexponentials, Synthetic Connectives, and
Multi-Level Delimited Control},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR)},
year = {2015},
editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver
and Andrei Voronkov},
month = nov,
doi = {10.1007/978-3-662-48899-7\_21},
series = {LNCS},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/subdelimlncs.pdf},
number = {9450},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@inproceedings{libal15cade,
author = {Tomer Libal},
title = {Regular Patterns in Second-Order Unification},
booktitle = {Automated Deduction - {CADE-25} - 25th International
Conference on Automated Deduction, Berlin, Germany,
August 1-7, 2015, Proceedings},
pages = {557--571},
year = {2015},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-pays = {DE},
x-international-audience = {yes},
x-proceedings = {yes}
}
@incollection{miller15appa,
author = {Dale Miller},
title = {Foundational Proof Certificates},
pages = {150--163},
year = {2015},
month = jan,
booktitle = {All about Proofs, Proofs for All},
editor = {David Delahaye and Bruno Woltzenlogel Paleo},
publisher = {College Publications},
address = {London, UK},
series = {Mathematical Logic and Foundations},
volume = {55},
isbn = {978-1-84890-166-7},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/appa2014.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{miller15lopstr,
author = {Dale Miller},
title = {Proof Checking and Logic Programming},
booktitle = {Logic-Based Program Synthesis and Transformation
(LOPSTR) 2015},
year = {2015},
editor = {Moreno Falaschi},
doi = {10.1007/978-3-319-27436-2\_1},
series = {LNCS},
number = {9527},
publisher = {Springer},
pages = {3--17},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes}
}
@inproceedings{miller15lpar,
author = {Dale Miller and Marco Volpe},
title = {Focused labeled proof systems for modal logic},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR)},
year = {2015},
editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver
and Andrei Voronkov},
series = {LNCS},
number = {9450},
doi = {10.1007/978-3-662-48899-7\_19},
pages = {266--280},
month = nov,
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@inproceedings{miller15ppdp,
author = {Dale Miller},
title = {Proof Checking and Logic Programming},
booktitle = {ACM SIGPLAN Conference on Principles and Practice of
Declarative Programming (PPDP)},
year = {2015},
editor = {Elvira Albert},
pages = {18},
month = jul,
doi = {10.1145/2790449.2790510},
publisher = {ACM},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes}
}
@inproceedings{reis15pxtp,
author = {Giselle Reis},
title = {Importing {SMT} and Connection proofs as expansion
trees},
year = {2015},
url = {http://arxiv.org/abs/1507.08715},
note = {Proof Exchange for Theorem Proving (PxTP)},
lixequipe = {Parsifal},
lixcategorie = {CIA}
}
@inproceedings{rouhling15frocos,
title = {Axiomatic constraint systems for proof search modulo
theories},
author = {Damien Rouhling and Mahfuza Farooque and St\'ephane
Graham-Lengrand and Assia Mahboubi and Jean-Marc
Notin},
editor = {Carsten Lutz and Silvio Ranise},
booktitle = {Proceedings of the 9th International Symposium on
Frontiers of Combining Systems (FroCoS'15)},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
year = {2015},
month = sep,
place = {Wroclaw, Poland},
lixequipe = {Parsifal},
lixcategorie = {CIA}
}
@inproceedings{wang15tlca,
author = {Yuting Wang and Kaustuv Chaudhuri},
title = {A Proof-Theoretic Characterization of Independence in
Type Theory},
booktitle = {Proceedings of the 13th International Conference on
Typed Lambda Calculi and Applications (TLCA)},
year = {2015},
editor = {Thorsten Altenkirch},
month = jul,
address = {Warsaw, Poland},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
pages = {332--346},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {US},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=5173},
doi = {10.4230/LIPIcs.TLCA.2015.332}
}
This file was generated by bibtex2html 1.98.