LIPIcs, Volume 188
TYPES 2020, March 2-5, 2020, University of Turin, Italy
Editors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Greta Coraglia and Jacopo Emmenegger. Categorical Models of Subtyping. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{coraglia_et_al:LIPIcs.TYPES.2023.3, author = {Coraglia, Greta and Emmenegger, Jacopo}, title = {{Categorical Models of Subtyping}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {3:1--3:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.3}, URN = {urn:nbn:de:0030-drops-204811}, doi = {10.4230/LIPIcs.TYPES.2023.3}, annote = {Keywords: dependent types, subtyping, coercive subtyping, categorical semantics, categories with families, monad} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2024.10, author = {Kaposi, Ambrus and Xie, Szumi}, title = {{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {10:1--10:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10}, URN = {urn:nbn:de:0030-drops-203396}, doi = {10.4230/LIPIcs.FSCD.2024.10}, annote = {Keywords: Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21, author = {Felicissimo, Thiago and Winterhalter, Th\'{e}o}, title = {{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {21:1--21:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21}, URN = {urn:nbn:de:0030-drops-203503}, doi = {10.4230/LIPIcs.FSCD.2024.21}, annote = {Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes} }
Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1
Pablo R. Fillottrani and C. Maria Keet. Logics for Conceptual Data Modelling: A Review. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Article{fillottrani_et_al:TGDK.2.1.4, author = {Fillottrani, Pablo R. and Keet, C. Maria}, title = {{Logics for Conceptual Data Modelling: A Review}}, journal = {Transactions on Graph Data and Knowledge}, pages = {4:1--4:30}, ISSN = {2942-7517}, year = {2024}, volume = {2}, number = {1}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.4}, URN = {urn:nbn:de:0030-drops-198616}, doi = {10.4230/TGDK.2.1.4}, annote = {Keywords: Conceptual Data Modelling, EER, UML, Description Logics, OWL} }
Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
Stefano Berardi, Gabriele Buriola, and Peter Schuster. A General Constructive Form of Higman’s Lemma. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{berardi_et_al:LIPIcs.CSL.2024.16, author = {Berardi, Stefano and Buriola, Gabriele and Schuster, Peter}, title = {{A General Constructive Form of Higman’s Lemma}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.16}, URN = {urn:nbn:de:0030-drops-196599}, doi = {10.4230/LIPIcs.CSL.2024.16}, annote = {Keywords: intuitionistic logic, constructive mathematics, formal proof, inductive predicate, bar induction, well quasi-order, Higman’s lemma} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1-204, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@Proceedings{deliguoro_et_al:LIPIcs.TYPES.2020, title = {{LIPIcs, Volume 188, TYPES 2020, Complete Volume}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {1--204}, 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}, URN = {urn:nbn:de:0030-drops-138785}, doi = {10.4230/LIPIcs.TYPES.2020}, annote = {Keywords: LIPIcs, Volume 188, TYPES 2020, Complete Volume} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{deliguoro_et_al:LIPIcs.TYPES.2020.0, author = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {0:i--0:viii}, 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.0}, URN = {urn:nbn:de:0030-drops-138792}, doi = {10.4230/LIPIcs.TYPES.2020.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{abel:LIPIcs.TYPES.2020.1, author = {Abel, Andreas}, title = {{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {1:1--1:21}, 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.1}, URN = {urn:nbn:de:0030-drops-138805}, doi = {10.4230/LIPIcs.TYPES.2020.1}, annote = {Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2, author = {Affeldt, Reynald and Nowak, David}, title = {{Extending Equational Monadic Reasoning with Monad Transformers}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {2:1--2:21}, 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.2}, URN = {urn:nbn:de:0030-drops-138810}, doi = {10.4230/LIPIcs.TYPES.2020.2}, annote = {Keywords: monads, monad transformers, Coq, impredicativity, parametricity} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Guido De Luca and Carlos Luna. Towards a Certified Reference Monitor of the Android 10 Permission System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{deluca_et_al:LIPIcs.TYPES.2020.3, author = {De Luca, Guido and Luna, Carlos}, title = {{Towards a Certified Reference Monitor of the Android 10 Permission System}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {3:1--3:18}, 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.3}, URN = {urn:nbn:de:0030-drops-138821}, doi = {10.4230/LIPIcs.TYPES.2020.3}, annote = {Keywords: Android, Permission model, Formal idealized model, Reference monitor, Formal proofs, Certified implementation, Coq} }
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 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{from:LIPIcs.TYPES.2020.5, author = {From, Asta Halkj{\ae}r}, title = {{Synthetic Completeness for a Terminating Seligman-Style Tableau System}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {5:1--5:17}, 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.5}, URN = {urn:nbn:de:0030-drops-138847}, doi = {10.4230/LIPIcs.TYPES.2020.5}, annote = {Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{hondet_et_al:LIPIcs.TYPES.2020.6, author = {Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric}, title = {{Encoding of Predicate Subtyping with Proof Irrelevance in the \lambda\Pi-Calculus Modulo Theory}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {6:1--6:18}, 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.6}, URN = {urn:nbn:de:0030-drops-138853}, doi = {10.4230/LIPIcs.TYPES.2020.6}, annote = {Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7, author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan}, title = {{\Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {7:1--7:18}, 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.7}, URN = {urn:nbn:de:0030-drops-138867}, doi = {10.4230/LIPIcs.TYPES.2020.7}, annote = {Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity} }
Feedback for Dagstuhl Publishing