@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -ob select2012.bib -c 'lixequipe : "Parsifal"' -c year=2012 master.bib}}
@misc{Abella,
key = {Abella},
title = {The {A}bella Prover},
note = {Available at \url{http://abella-prover.org/}},
year = {2012},
lixequipe = {Parsifal},
lixcategorie = {SW}
}
@inproceedings{accattoli12cpp,
author = {Beniamino Accattoli},
title = {Proof pearl: Abella formalization of lambda calculus
cube property},
booktitle = {Second International Conference on Certified Programs
and Proofs},
editor = {Chris Hawblitzel and Dale Miller},
year = {2012},
publisher = {Springer},
series = {LNCS},
volume = {7679},
pages = {173--187},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{accattoli12flops,
author = {Beniamino Accattoli and Luca Paolini},
title = {Call-by-Value Solvability, Revisited},
booktitle = {Eleventh International Symposium on Functional and
Logic Programming (FLOPS 2012)},
editors = {Tom Schrijvers and Peter Thiemann},
year = {2012},
pages = {4--16},
doi = {10.1007/978-3-642-29822-6\_4},
publisher = {Springer},
series = {LNCS},
volume = {7294},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {IT},
x-international-audience = {yes},
x-proceedings = {yes}
}
@article{accattoli12lmcs,
author = {Beniamino Accattoli and Delia Kesner},
title = {Preservation of Strong Normalisation modulo
permutations for the structural lambda-calculus},
journal = {Logical Methods in Computer Science},
volume = {8},
number = {1},
year = {2012},
doi = {10.2168/LMCS-8(1:28)2012},
url = {http://hal.archives-ouvertes.fr/hal-00686780},
lixcategorie = {RI},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {article},
x-support = {revue}
}
@inproceedings{accattoli12lpar,
author = {Beniamino Accattoli and Delia Kesner},
title = {The Permutative $\lambda$-Calculus},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning - 18th International Conference (LPAR-18)},
year = {2012},
editors = {Nikolaj Bjørner and Andrei Voronkov},
pages = {23--36},
doi = {10.1007/978-3-642-28717-6\_5},
publisher = {Springer},
series = {LNCS},
volume = {7180},
url = {http://hal.archives-ouvertes.fr/hal-00686795},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{accattoli12rtaa,
author = {Beniamino Accattoli and Ugo Dal Lago},
title = {On the Invariance of the Unitary Cost Model for Head
Reduction},
booktitle = {23rd International Conference on Rewriting Techniques
and Applications (RTA)},
editor = {Ashish Tiwari},
year = {2012},
pages = {22--37},
doi = {10.4230/LIPIcs.RTA.2012.22},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
volume = {15},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {IT},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{accattoli12rtab,
author = {Beniamino Accattoli},
title = {An Abstract Factorization Theorem for Explicit
Substitutions},
booktitle = {23rd International Conference on Rewriting Techniques
and Applications (RTA)},
editor = {Ashish Tiwari},
year = {2012},
pages = {6--21},
doi = {10.4230/LIPIcs.RTA.2012.6},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
volume = {15},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{chaudhuri12cpp,
author = {Kaustuv Chaudhuri},
title = {Compact Proof Certificates for Linear Logic},
booktitle = {Proceedings of the Second Internatinal Conference on
Certified Programs and Proofs (CPP)},
editor = {Chris Hawblitzel and Dale Miller},
year = {2012},
month = dec,
publisher = {Springer},
series = {LNCS},
volume = {7679},
pages = {208--223},
address = {Kyoto, Japan},
doi = {10.1007/978-3-642-35308-6\_17},
hal_id = {hal-00760118},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-international-audience = {yes},
x-proceedings = {yes},
url = {http://kaustuv.chaudhuri.info/papers/cpp12deepcert.pdf}
}
@inproceedings{chaudhuri12csl,
author = {Kaustuv Chaudhuri and Stefan Hetzl and Dale Miller},
title = {A Systematic Approach to Canonicity in the Classical
Sequent Calculus},
booktitle = {CSL 2012: Computer Science Logic},
year = {2012},
month = sep,
pages = {183--197},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
volume = {16},
doi = {10.4230/LIPIcs.CSL.2012.183},
isbn = {978-3-939897-42-2},
issn = {1868-8969},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {AT},
x-international-audience = {yes},
x-proceedings = {yes}
}
@techreport{farooque12tr,
url = {http://hal.archives-ouvertes.fr/hal-00690044},
title = {{Two simulations about DPLL(T)}},
author = {Mahfuza Farooque and St{\'e}phane Lengrand and Assia
Mahboubi},
institution = {Laboratoire d'informatique de l'{\'e}cole
polytechnique - LIX, CNRS-Ecole Polytechnique-INRIA},
collaboration = {Project PSI: Proof-Search control in Interaction with
domain-specific methods},
year = {2012},
month = mar,
lixequipe = {Parsifal},
lixcategorie = {RT}
}
@techreport{farooque12trb,
url = {http://hal.inria.fr/hal-00690392},
title = {{Simulating the DPLL(T) procedure in a sequent
calculus with focusing}},
author = {Mahfuza Farooque and St{\'e}phane Lengrand and Assia
Mahboubi},
institution = {Laboratoire d'informatique de l'{\'e}cole
polytechnique - LIX, CNRS-Ecole Polytechnique-INRIA},
year = {2012},
month = mar,
lixequipe = {Parsifal},
lixcategorie = {RT}
}
@article{gacek12jar,
author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
title = {A two-level logic approach to reasoning about
computations},
year = {2012},
url = {http://arxiv.org/abs/0911.2993},
doi = {10.1007/s10817-011-9218-1},
journal = {J. of Automated Reasoning},
volume = {49},
number = {2},
pages = {241--273},
lixcategorie = {RI},
lixequipe = {Parsifal},
x-pays = {US}
}
@inproceedings{gazeau12qapl,
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
title = {A non-local method for robustness analysis of floating
point programs},
booktitle = {Proceedings of the 10th Workshop on Quantitative
Aspects of Programming Languages and Systems (QAPL
2012)},
pages = {63--76},
year = {2012},
editor = {Herbert Wiklicky and Mieke Massink},
volume = {85},
series = {Electronic Proceedings in Theoretical Computer
Science},
doi = {10.4204/EPTCS.85.5},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {QAPL}
}
@proceedings{gramlich12ijcar,
title = {Automated Reasoning: 6th International Joint
Conference, {IJCAR} 2012, Manchester, {UK}, June 2012,
Proceedings},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Uli Sattler},
volume = {7364},
series = {LNAI},
publisher = {Springer},
doi = {10.1007/978-3-642-31365-3},
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}
}
@proceedings{hawblitzel12cpp,
title = {{CPP}: Second International Conference on Certified
Programs and Proofs},
year = {2012},
editor = {Chris Hawblitzel and Dale Miller},
volume = {7679},
series = {LNCS},
publisher = {Springer},
doi = {10.1007/978-3-642-35308-6},
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}
}
@inproceedings{hetzl12cicm,
author = {Stefan Hetzl},
title = {{Project Presentation: Algorithmic Structuring and
Compression of Proofs (ASCOP)}},
booktitle = {Conference on Intelligent Computer Mathematics (CICM)
2012},
editor = {J. Jeuring et al.},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
volume = {7362},
year = {2012},
pages = {437--441},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{hetzl12csl,
author = {Stefan Hetzl and Lutz Stra{\ss}burger},
title = {{H}erbrand-{C}onfluence for {C}ut-{E}limination in
{C}lassical {F}irst-{O}rder {L}ogic},
booktitle = {Computer Science Logic (CSL) 2012},
pages = {320--334},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
volume = {16},
year = {2012},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {AT},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{lamarche12jal,
hal_id = {hal-00706562},
url = {http://hal.inria.fr/hal-00706562},
title = {{Modelling Martin L{\"o}f Type Theory in Categories}},
author = {Fran{\c c}ois Lamarche},
keywords = {Martin-L{\"o}f type theory, Grothendieck Fibration,
Martin-L{\"o}f identity type, abstract homotopy theory,
path object.},
language = {Anglais},
affiliation = {PARSIFAL - INRIA Saclay - Ile de France},
booktitle = {{Logic, Categories, Semantics, special issue of J. of
Applied Logic}},
publisher = {Elsevier North-Holland},
address = {Bordeaux, France},
organization = {Ch. Retor{\'e} and J. Gilibert},
note = {Scheduled to appear in June 2013},
editor = {Ch. Retor{\'e} and J. Gilibert},
year = {2012},
month = jun,
pdf = {http://hal.inria.fr/hal-00706562/PDF/IdentityTypeMyElsev.pdf},
lixcategorie = {RI},
lixequipe = {Parsifal}
}
@proceedings{miller12fics,
title = {Proceedings 8th Workshop on Fixed Points in Computer
Science},
year = {2012},
editor = {Dale Miller and Zolt\'{a}n \'{E}sik},
doi = {10.4204/EPTCS.77},
url = {http://eptcs.org/Published/FICS2012/Proceedings.pdf},
volume = {77},
series = {Electronic Proceedings in Theoretical Computer
Science},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@book{miller12proghol,
author = {Dale Miller and Gopalan Nadathur},
title = {Programming with Higher-Order Logic},
publisher = {Cambridge University Press},
year = {2012},
month = jun,
doi = {10.1017/CBO9781139021326},
lixcategorie = {OUV},
lixequipe = {Parsifal},
aeres = {Dummy Field},
x-equipes = {parsifal EXT},
x-type = {livre},
x-editorial-board = {no},
x-proceedings = {no},
x-international-audience = {yes},
x-invited-conference = {no},
x-scientific-popularization = {yes}
}
@misc{psyche,
key = {Psyche},
title = {Psyche: the {Proof-Search factorY for Collaborative
HEuristics}},
note = {Available at
\url{http://www.lix.polytechnique.fr/~lengrand/Psyche}},
year = {2012},
lixequipe = {Parsifal},
lixcategorie = {SW}
}
@article{strassburger12apal,
author = {Lutz Stra{\ss}burger},
title = {Extension without Cut},
publisher = {Elsevier},
pages = {1995--2007},
journal = {Annals of Pure and Applied Logic},
volume = {163},
number = {12},
x-international-audience = {yes},
doi = {10.1016/j.apal.2012.07.004},
year = {2012},
url = {http://hal.inria.fr/hal-00759215},
pdf = {http://hal.inria.fr/hal-00759215/PDF/psppp.pdf},
lixequipe = {Parsifal},
lixcategorie = {RI}
}
This file was generated by bibtex2html 1.98.