@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -ob select2013.bib -c 'lixequipe : "Parsifal"' -c year=2013 master.bib}}
@misc{Profound,
title = {Profound: a linking-based interactive prover},
note = {Available at:
\url{http://chaudhuri.info/software/profound/}},
year = {2013},
author = {Kaustuv Chaudhuri},
lixequipe = {Parsifal},
lixcategorie = {SW}
}
@unpublished{bernadet13a,
author = {Alexis Bernadet and {St\'ephane} Graham-Lengrand},
title = {A big-step operational semantics via non-idempotent
intersection types},
year = {2013},
month = apr,
note = {Submitted},
lixequipe = {Parsifal},
lixcategorie = {AU}
}
@article{bernadet13lmcs,
author = {Alexis Bernadet and {St\'ephane} Graham-Lengrand},
title = {Non-idempotent intersection types and strong
normalisation},
year = {2013},
journal = {Logical Methods in Computer Science},
volume = {9},
number = {4},
doi = {10.2168/LMCS-9(4:3)2013},
url = {http://arxiv.org/abs/1310.1622},
lixequipe = {Parsifal},
lixcategorie = {AU}
}
@inproceedings{burel13pxtp,
author = {Guillaume Burel},
title = {A Shallow Embedding of Resolution and Superposition
Proofs into the $\lambda{\Pi}$-Calculus Modulo},
booktitle = {Third International Workshop on Proof Exchange for
Theorem Proving (PxTP 2013)},
pages = {43--57},
year = {2013},
editor = {J. C. Blanchette and J. Urban},
volume = {14},
series = {EPiC Series},
publisher = {EasyChair},
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{chaudhuri13itp,
author = {Kaustuv Chaudhuri},
title = {Subformula Linking as an Interaction Method},
booktitle = {Proceedings of the 4th Conference on Interactive
Theorem Proving (ITP)},
year = {2013},
month = jul,
editor = {Sandrine Blazy and Christine Paulin-Mohring and David
Pichardie},
series = {LNCS},
volume = {7998},
pages = {386--401},
publisher = {Springer},
url = {http://chaudhuri.info/papers/itp13link.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {ITP},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@misc{chaudhuri13types,
author = {Kaustuv Chaudhuri and Jo{\"e}lle Despeyroux},
title = {A Hybrid Linear Logic for Constrained Transition
Systems},
howpublished = {Collected Abstracts of the 19th Conference on Types
for Proofs and Programs (TYPES)},
year = {2013},
month = apr,
url = {http://chaudhuri.info/papers/abst13hyll.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {TYPES},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@misc{chaudhuri13url,
title = {{TLAPS}: the {TLA$^+$} proof system},
author = {Kaustuv Chaudhuri and Denis Cousineau and Damien
Doligez and Markus Kuppe and Leslie Lamport and Tomer
Libal and Stephan Merz and Hern{\'a}n Vanzetto},
year = {2013},
note = {Available from
\url{http://tla.msr-inria.inria.fr/tlaps/}},
lixequipe = {Parsifal},
lixcategorie = {SW}
}
@inproceedings{chihani13cade,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {Foundational proof certificates in first-order logic},
booktitle = {CADE 24: Conference on Automated Deduction 2013},
year = {2013},
editor = {Maria Paola Bonacina},
series = {LNAI},
number = {7898},
pages = {162--177},
lixcategorie = {CIA},
lixequipe = {Parsifal},
doi = {10.1007/978-3-642-38574-2\_11},
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{chihani13pxtp,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {Checking Foundational Proof Certificates for
First-Order Logic (extended abstract)},
booktitle = {Third International Workshop on Proof Exchange for
Theorem Proving (PxTP 2013)},
pages = {58--66},
year = {2013},
editor = {J. C. Blanchette and J. Urban},
volume = {14},
series = {EPiC Series},
publisher = {EasyChair},
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{farooque13lfmtp,
author = {Mahfuza Farooque and {St\'ephane} Graham-Lengrand and
Assia Mahboubi},
title = {A bisimulation between {DPLL(T)} and a proof-search
strategy for the focused sequent calculus},
booktitle = {Proceedings of the 2013 ACM SIGPLAN Workshop on
Logical Frameworks~\& Meta-Languages: Theory~\&
Practice, LFMTP'13},
pages = {3--13},
year = {2013},
editor = {Alberto Momigliano and Brigitte Pientka and Randy
Pollack},
month = sep,
publisher = {ACM},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lfmtp13.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-proceedings = {yes},
aeres = {Dummy Field},
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}
}
@phdthesis{farooque13phd,
author = {Mahfuza Farooque},
title = {Automated reasoning techniques in sequent calculus},
school = {Ecole Polytechnique},
year = {2013},
type = {Ph.D. Thesis},
lixequipe = {Parsifal},
lixcategorie = {TH}
}
@techreport{farooque13tr,
title = {Sequent calculi with procedure calls},
author = {Mahfuza Farooque and St{\'e}phane Graham-Lengrand},
year = {2013},
month = jan,
institution = {Laboratoire d'informatique de l'{\'e}cole
polytechnique - LIX, CNRS-Ecole Polytechnique-INRIA},
url = {http://hal.archives-ouvertes.fr/hal-00779199},
collaboration = {Project PSI: Proof-Search control in Interaction with
domain-specific methods},
lixequipe = {Parsifal},
lixcategorie = {RT}
}
@phdthesis{gazeau13phd,
author = {Ivan Gazeau},
title = {Safe Programming in finite precision: Controling the
errors and information leaks},
school = {Ecole Polytechnique},
year = {2013},
type = {Ph.D. Thesis},
lixequipe = {Parsifal},
lixcategorie = {TH}
}
@inproceedings{gazeau13qapl,
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
title = {Preserving differential privacy under finite-precision
semantics},
booktitle = {Proceedings 11th International Workshop on
Quantitative Aspects of Programming Languages and
Systems (QAPL)},
hal = {http://hal.inria.fr/hal-00780774},
url = {http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?QAPL2013},
year = {2013},
pages = {1--18},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {QAPL},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@proceedings{grahamlengrand13itrs,
editor = {St{\'e}phane Graham-Lengrand and Luca Paolini},
title = {Proceedings Sixth Workshop on Intersection Types and
Related Systems, {ITRS} 2013, Dubrovnik, Croatia, 29th
June 2012},
series = {EPTCS},
volume = {121},
year = {2013},
doi = {10.4204/EPTCS.121},
lixcategorie = {OUV},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {livre},
x-support = {actes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@phdthesis{guenot13phd,
author = {Nicolas Guenot},
school = {Ecole Polytechnique},
title = {Nested Deduction in Logical Foundations for
Computation},
type = {Ph.D. Thesis},
year = {2013},
lixequipe = {Parsifal},
lixcategorie = {TH}
}
@techreport{lamarche13hal,
hal_id = {hal-00831430},
url = {http://hal.inria.fr/hal-00831430},
title = {{Path Functors in Cat}},
author = {Fran{\c c}ois Lamarche},
institution = {INRIA},
number = {hal-00831430},
abstract = {{We build an endofunctor in the category of small
categories along with the necessary structure on it to
turn it into a path object suitable for homotopy theory
and modelling identity types in Martin-L\"of type
theory. We construct the free Grothendieck bifibration
over a base category generated by an arbitrary functor
to that category.}},
language = {Anglais},
affiliation = {PARSIFAL - INRIA Saclay - Ile de France},
pdf = {http://hal.inria.fr/hal-00831430/PDF/PathFunctorsInCat.pdf},
lixcategorie = {RT},
lixequipe = {Parsifal},
note = {Submitted},
month = apr,
year = {2013}
}
@inproceedings{lengrand13tableaux,
title = {{Psyche}: a proof-search engine based on sequent
calculus with an {LCF}-style architecture},
author = {{St\'ephane} Graham-Lengrand},
year = {2013},
editor = {Didier Galmiche and Dominique Larchey-Wendling},
booktitle = {International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods (Tableaux'13)},
publisher = {Springer},
series = {LNCS},
volume = {8123},
pages = {149--156},
month = sep,
place = {Nancy, France},
lixcategorie = {CIA},
lixequipe = {Parsifal}
}
@article{liang13apal,
author = {Chuck Liang and Dale Miller},
title = {Kripke Semantics and Proof Systems for Combining
Intuitionistic Logic and Classical Logic},
journal = {Annals of Pure and Applied Logic},
month = feb,
year = {2013},
doi = {10.1016/j.apal.2012.09.005},
volume = {164},
number = {2},
pages = {86--111},
url = {http://hal.inria.fr/hal-00787601},
lixcategorie = {RI},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {article},
x-support = {revue}
}
@inproceedings{liang13lics,
author = {Chuck Liang and Dale Miller},
title = {Unifying Classical and Intuitionistic Logics for
Computational Control},
booktitle = {28th Symp.\ on Logic in Computer Science},
year = {2013},
editor = {Orna Kupferman},
pages = {283--292},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {US},
aeres = {Dummy Field},
hal = {http://hal.inria.fr/hal-00906299},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics13.pdf},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {LICS},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{miller13cpp,
author = {Dale Miller and Alwen Tiu},
title = {Extracting Proofs from Tabled Proof Search},
booktitle = {Certified Programs and Proofs},
year = {2013},
editor = {Georges Gonthier and Michael Norrish},
month = dec,
publisher = {Springer},
series = {LNCS},
number = {8307},
pages = {194--210},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cpp2013.pdf},
hal = {http://hal.inria.fr/hal-00863561/},
address = {Melburne, Australia},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{miller13lfmtp,
author = {Dale Miller},
title = {Foundational Proof Certificates: Making Proof
Universal and Permanent},
booktitle = {Proceedings of the 2013 ACM SIGPLAN Workshop on
Logical Frameworks~\& Meta-Languages: Theory~\&
Practice, LFMTP'13},
pages = {1},
year = {2013},
editor = {Alberto Momigliano and Brigitte Pientka and Randy
Pollack},
month = sep,
publisher = {ACM},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lfmtp13.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-proceedings = {yes},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {article},
x-support = {actes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {yes},
x-scientific-popularization = {no}
}
@article{miller13tcs,
author = {Dale Miller and Elaine Pimentel},
title = {A formal framework for specifying sequent calculus
proof systems},
journal = {Theoretical Computer Science},
year = {2013},
doi = {10.1016/j.tcs.2012.12.008},
volume = {474},
pages = {98--116},
lixcategorie = {RI},
lixequipe = {Parsifal},
url = {http://hal.inria.fr/hal-00787586}
}
@inproceedings{strassburger13fossacs,
author = {Lutz Stra{\ss}burger},
title = {Cut Elimination in Nested Sequents for Intuitionistic
Modal Logics},
booktitle = {Foundations of Software Science and Computation
Structures, 16th International Conference (FOSSACS)},
year = {2013},
editor = {Frank Pfenning},
volume = {7794},
series = {LNCS},
pages = {209--224},
publisher = {Springer},
doi = {10.1007/978-3-642-37075-5\_14},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {FOSSACS},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{wang13ppdp,
author = {Yuting Wang and Kaustuv Chaudhuri and Andrew Gacek and
Gopalan Nadathur},
title = {Reasoning about Higher-Order Relational
Specifications},
booktitle = {Proceedings of the 15th International Symposium on
Princples and Practice of Declarative Programming
(PPDP)},
year = {2013},
month = sep,
editor = {Tom Schrijvers},
pages = {157--168},
doi = {10.1145/2505879.2505889},
address = {Madrid, Spain},
url = {http://chaudhuri.info/papers/draft13hhw.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal},
x-type = {article},
x-support = {actes},
x-cle-support = {ITP},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {US},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
This file was generated by bibtex2html 1.98.