LIPIcs, Volume 130
TYPES 2018, June 18-21, 2018, Braga, Portugal
Editors: Peter Dybjer, José Espírito Santo, and Luís Pinto
Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3, author = {Pimentel, Elaine and Pereira, Luiz Carlos}, title = {{A Tour on Ecumenical Systems}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {3:1--3:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3}, URN = {urn:nbn:de:0030-drops-188003}, doi = {10.4230/LIPIcs.CALCO.2023.3}, annote = {Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
José Espírito Santo and Filipa Mendes. The Logical Essence of Compiling with Continuations. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 19:1-19:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2023.19, author = {Esp{\'\i}rito Santo, Jos\'{e} and Mendes, Filipa}, title = {{The Logical Essence of Compiling with Continuations}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {19:1--19:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.19}, URN = {urn:nbn:de:0030-drops-180036}, doi = {10.4230/LIPIcs.FSCD.2023.19}, annote = {Keywords: Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2020.4, author = {Esp{\'\i}rito Santo, Jos\'{e} and Matthes, Ralph and Pinto, Lu{\'\i}s}, title = {{Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {4:1--4:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-182-5}, ISSN = {1868-8969}, year = {2021}, volume = {188}, editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.4}, URN = {urn:nbn:de:0030-drops-138837}, doi = {10.4230/LIPIcs.TYPES.2020.4}, annote = {Keywords: Inhabitation problems, Coinduction, Lambda-calculus, Polarized logic} }
Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
José Espírito Santo. The Call-By-Value Lambda-Calculus with Generalized Applications. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 35:1-35:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{espiritosanto:LIPIcs.CSL.2020.35, author = {Esp{\'\i}rito Santo, Jos\'{e}}, title = {{The Call-By-Value Lambda-Calculus with Generalized Applications}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {35:1--35:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.35}, URN = {urn:nbn:de:0030-drops-116786}, doi = {10.4230/LIPIcs.CSL.2020.35}, annote = {Keywords: Generalized applications, Natural deduction, Strong normalization, Standardization, Call-by-name, Call-by-value, Protecting-by-a-lambda} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Peter Dybjer, José Espírito Santo, and Luís Pinto. LIPIcs, Volume 130, TYPES'18, Complete Volume. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018, title = {{LIPIcs, Volume 130, TYPES'18, Complete Volume}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018}, URN = {urn:nbn:de:0030-drops-114507}, doi = {10.4230/LIPIcs.TYPES.2018}, annote = {Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Peter Dybjer, José Espírito Santo, and Luís Pinto. Front Matter, Table of Contents, Preface, Conference Organization. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 0:i-0:x, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0, author = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0}, URN = {urn:nbn:de:0030-drops-114045}, doi = {10.4230/LIPIcs.TYPES.2018.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal Embeddings and Calling Paradigms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 18:1-18:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2019.18, author = {Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s and Uustalu, Tarmo}, title = {{Modal Embeddings and Calling Paradigms}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {18:1--18:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.18}, URN = {urn:nbn:de:0030-drops-105256}, doi = {10.4230/LIPIcs.FSCD.2019.18}, annote = {Keywords: intuitionistic S4, call-by-name, call-by-value, comonadic lambda-calculus, standardization, indifference property} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
José Espírito Santo, Maria João Frade, and Luís Pinto. Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 10:1-10:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2016.10, author = {Esp{\'\i}rito Santo, Jos\'{e} and Frade, Maria Jo\~{a}o and Pinto, Lu{\'\i}s}, title = {{Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {10:1--10:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.10}, URN = {urn:nbn:de:0030-drops-98523}, doi = {10.4230/LIPIcs.TYPES.2016.10}, annote = {Keywords: sequent calculus, permutative conversion, Curry-Howard isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
José Espírito Santo. Curry-Howard for Sequent Calculus at Last!. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 165-179, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
@InProceedings{espiritosanto:LIPIcs.TLCA.2015.165, author = {Esp{\'\i}rito Santo, Jos\'{e}}, title = {{Curry-Howard for Sequent Calculus at Last!}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {165--179}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.165}, URN = {urn:nbn:de:0030-drops-51626}, doi = {10.4230/LIPIcs.TLCA.2015.165}, annote = {Keywords: co-control, co-continuation, vector notation, let-expression, formal sub- stitution, context substitution, computational lambda-calculus, classical lo} }
Feedback for Dagstuhl Publishing