Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé's Longstanding Conjecture. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{intrigila_et_al:LIPIcs.FSCD.2017.20, author = {Intrigila, Benedetto and Manzonetto, Giulio and Polonsky, Andrew}, title = {{Refutation of Sall\'{e}'s Longstanding Conjecture}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.20}, URN = {urn:nbn:de:0030-drops-77236}, doi = {10.4230/LIPIcs.FSCD.2017.20}, annote = {Keywords: lambda calculus, observational equivalence, B\"{o}hm trees, omega-rule} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{breuvart_et_al:LIPIcs.FSCD.2016.15, author = {Breuvart, Flavien and Manzonetto, Giulio and Polonsky, Andrew and Ruoppolo, Domenico}, title = {{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {15:1--15:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, year = {2016}, volume = {52}, editor = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15}, URN = {urn:nbn:de:0030-drops-59924}, doi = {10.4230/LIPIcs.FSCD.2016.15}, annote = {Keywords: Lambda calculus, relational models, fully abstract, B\"{o}hm-out, omega-rule} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Andrew Polonsky. Extensionality of lambda-*. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 221-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{polonsky:LIPIcs.TYPES.2014.221, author = {Polonsky, Andrew}, title = {{Extensionality of lambda-*}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {221--250}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.221}, URN = {urn:nbn:de:0030-drops-54995}, doi = {10.4230/LIPIcs.TYPES.2014.221}, annote = {Keywords: Extensionality, logical relations, type theory, lambda calculus, reflection} }
Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.143, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {143--159}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143}, URN = {urn:nbn:de:0030-drops-51949}, doi = {10.4230/LIPIcs.RTA.2015.143}, annote = {Keywords: infinitary rewriting, coinduction} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
Jörg Endrullis and Andrew Polonsky. Infinitary Rewriting Coinductively. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 16-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{endrullis_et_al:LIPIcs.TYPES.2011.16, author = {Endrullis, J\"{o}rg and Polonsky, Andrew}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {16--27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.16}, URN = {urn:nbn:de:0030-drops-38971}, doi = {10.4230/LIPIcs.TYPES.2011.16}, annote = {Keywords: infinitary rewriting, coinduction, lambda calculus, standardization} }
Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)
Andrew Polonsky. Axiomatizing the Quote. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 458-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
@InProceedings{polonsky:LIPIcs.CSL.2011.458, author = {Polonsky, Andrew}, title = {{Axiomatizing the Quote}}, booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL}, pages = {458--469}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-32-3}, ISSN = {1868-8969}, year = {2011}, volume = {12}, editor = {Bezem, Marc}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.458}, URN = {urn:nbn:de:0030-drops-32493}, doi = {10.4230/LIPIcs.CSL.2011.458}, annote = {Keywords: lambda calculus, combinatory logic, quote operator, enumerator} }