alan-journal.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bib2bib -ob alan-journal.bib -oc alan-journal.keys -c '(Alan:"1") & ($type="ARTICLE")' --rename journaltitle journal alan.bib}}

@article{FosterGreenwaldKirkegaardPierceSchmitt2007,
  alan = 1,
  author = {J. Nathan Foster and Michael B. Greenwald and Christian Kirkegaard and Benjamin C. Pierce and Alan Schmitt},
  date-added = {2007-07-23 14:18:06 +0200},
  date-modified = {2010-06-07 16:33:57 +0200},
  doi = {http://dx.doi.org/10.1016/j.jcss.2006.10.024},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/sync-jcss.pdf},
  journal = {Journal of Computer and System Sciences},
  keywords = {Harmony},
  month = jun,
  note = {Extended abstract in {\em Database Programming Languages (DBPL)} 2005},
  number = 4,
  pages = {669--689},
  read = 1,
  short = {http://www.cis.upenn.edu/~bcpierce/papers/sync-dbpl.pdf},
  slides = {http://www.cis.upenn.edu/~jnfoster/papers/schema-sync-slides.pdf},
  title = {Exploiting Schemas in Data Synchronization},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/sync-tr.pdf},
  volume = 73,
  year = 2007
}

@article{FosterGreenwaldMoorePierceSchmitt2007,
  address = {New York, NY, USA},
  alan = 1,
  author = {J. Nathan Foster and Michael B. Greenwald and Jonathan T.
                  Moore and Benjamin C. Pierce and Alan Schmitt},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-toplas-final.pdf},
  fullappendix = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-toplas-electronic-appendix.pdf},
  journal = {ACM Transactions on Programming Languages and Systems},
  month = may,
  note = {Extended abstract in {\em Principles of Programming Languages (POPL)}, 2005},
  number = 3,
  pages = 17,
  publisher = {ACM Press},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl-slides.pdf},
  title = {Combinators for bidirectional tree transformations:
                  A linguistic approach to the view-update problem},
  volume = 29,
  year = 2007
}

@article{GenevèsGesbertLayaïdaSchmitt2015,
  publisher = {Association for Computing Machinery},
  doi = {10.1145/2724712},
  number = 2,
  volume = 16,
  alan = 1,
  author = {Genevès, Pierre and Gesbert, Nils and Layaïda, Nabil and Schmitt, Alan},
  hal = {https://hal.inria.fr/hal-00868722},
  journal = {ACM Transactions on Computational Logic},
  title = {Efficiently Deciding $\mu$-calculus with Converse over Finite Trees},
  year = 2015
}

@article{LanesePérezSangiorgiSchmitt2011,
  alan = 1,
  author = {Lanese, Ivan and Pérez, Jorge A and Sangiorgi, Davide and Schmitt, Alan},
  full = {http://www.irisa.fr/celtique/aschmitt/papers/Lanese2011On-the-Expressivenes.pdf},
  journal = {Information and Computation},
  month = feb,
  note = {Extended abstract in \emph{Logic in Computer Science (LICS)}, 2008. Coq formalization available at \url{http://www.irisa.fr/celtique/aschmitt/research/hocore/}},
  number = 2,
  pages = {198--226},
  read = 1,
  title = {On the Expressiveness and Decidability of Higher-Order Process Calculi},
  volume = 209,
  year = 2011
}

@article{LengletSchmittStefani2011,
  alan = 1,
  author = {Lenglet, Sergueï and Schmitt, Alan and Stefani, Jean-Bernard},
  date-added = {2011-10-13 10:07:33 +0000},
  date-modified = {2013-10-16 13:47:12 +0000},
  doi = {http://dx.doi.org/10.1016/j.ic.2011.08.002},
  full = {http://www.irisa.fr/celtique/aschmitt/papers/Lenglet2011Characterizing-Conte.pdf},
  journal = {Information and Computation},
  month = nov,
  note = {Extended abstract in \emph{FOSSACS}, 2009, and \emph{CONCUR}, 2009.},
  number = 11,
  pages = {1390--1433},
  read = 1,
  title = {Characterizing Contextual Equivalence in Calculi with Passivation},
  volume = 209,
  year = 2011,
  abstract = {We study the problem of characterizing contextual equivalence in higher-order languages with passivation. To overcome the difficulties arising in the proof of congruence of candidate bisimilarities, we introduce a new form of labeled transition semantics together with its associated notion of bisimulation, which we call complementary semantics. Complementary semantics allows to apply the well-known Howeʼs method for proving the congruence of bisimilarities in a higher-order setting, even in the presence of an early form of bisimulation. We use complementary semantics to provide a coinductive characterization of contextual equivalence in the HOπP calculus, an extension of the higher-order π-calculus with passivation, obtaining the first result of this kind. We then study the problem of defining a more effective variant of bisimilarity that still characterizes contextual equivalence, along the lines of Sangiorgiʼs notion of normal bisimilarity. We provide partial results on this difficult problem: we show that a large class of test processes cannot be used to derive a normal bisimilarity in HOπP, but we show that a form of normal bisimilarity can be defined for HOπP without restriction.

}
}

@article{AmbalLengletSchmitt2020,
  title = {{HO$\pi$ in Coq}},
  author = {Ambal, Guillaume and Lenglet, Sergueï and Schmitt, Alan},
  hal = {https://hal.inria.fr/hal-02536463},
  journal = {{Journal of Automated Reasoning}},
  publisher = {{Springer Verlag}},
  year = 2020,
  doi = {10.1007/s10817-020-09553-0},
  keywords = {Coq ; Higher-order process calculus ; Howe's method},
  pdf = {https://hal.inria.fr/hal-02536463v2/file/jar.pdf},
  hal_id = {hal-02536463},
  hal_version = {v2},
  alan = 1
}

@comment{{Local Variables:
  bibtex-dialect: biblatex
  End:
}}