Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{grienenberger:LIPIcs.TYPES.2022.4, author = {Grienenberger, Emilie}, title = {{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4}, URN = {urn:nbn:de:0030-drops-184479}, doi = {10.4230/LIPIcs.TYPES.2022.4}, annote = {Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics} }
Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19, author = {Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar}, title = {{Translating Proofs from an Impredicative Type System to a Predicative One}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {19:1--19:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.19}, URN = {urn:nbn:de:0030-drops-174801}, doi = {10.4230/LIPIcs.CSL.2023.19}, annote = {Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21, author = {D{\'\i}az-Caro, Alejandro and Dowek, Gilles}, title = {{Linear Lambda-Calculus is Linear}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {21:1--21:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21}, URN = {urn:nbn:de:0030-drops-163024}, doi = {10.4230/LIPIcs.FSCD.2022.21}, annote = {Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{felicissimo:LIPIcs.FSCD.2022.25, author = {Felicissimo, Thiago}, title = {{Adequate and Computational Encodings in the Logical Framework Dedukti}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {25:1--25:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.25}, URN = {urn:nbn:de:0030-drops-163064}, doi = {10.4230/LIPIcs.FSCD.2022.25}, annote = {Keywords: Type Theory, Logical Frameworks, Rewriting, Dedukti, Pure Type Systems} }
Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20, author = {Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois}, title = {{Some Axioms for Mathematics}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20}, URN = {urn:nbn:de:0030-drops-142581}, doi = {10.4230/LIPIcs.FSCD.2021.20}, annote = {Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty} }
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-dev.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 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Alejandro Díaz-Caro and Gilles Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2019.14, author = {D{\'\i}az-Caro, Alejandro and Dowek, Gilles}, title = {{Proof Normalisation in a Logic Identifying Isomorphic Propositions}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {14:1--14:23}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.14}, URN = {urn:nbn:de:0030-drops-105210}, doi = {10.4230/LIPIcs.FSCD.2019.14}, annote = {Keywords: Simply typed lambda calculus, Isomorphisms, Logic, Cut-elimination, Proof-reduction} }
Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Gilles Dowek. Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 109:1-109:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{dowek:LIPIcs.ICALP.2017.109, author = {Dowek, Gilles}, title = {{Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory}}, booktitle = {44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)}, pages = {109:1--109:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-041-5}, ISSN = {1868-8969}, year = {2017}, volume = {80}, editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.109}, URN = {urn:nbn:de:0030-drops-73919}, doi = {10.4230/LIPIcs.ICALP.2017.109}, annote = {Keywords: model, proof reduction, Simple type theory, Calculus of constructions} }
Published in: Dagstuhl Reports, Volume 6, Issue 10 (2017)
Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe. Universality of Proofs (Dagstuhl Seminar 16421). In Dagstuhl Reports, Volume 6, Issue 10, pp. 75-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@Article{dowek_et_al:DagRep.6.10.75, author = {Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian}, title = {{Universality of Proofs (Dagstuhl Seminar 16421)}}, pages = {75--98}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2017}, volume = {6}, number = {10}, editor = {Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.10.75}, URN = {urn:nbn:de:0030-drops-69514}, doi = {10.4230/DagRep.6.10.75}, annote = {Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability} }
Feedback for Dagstuhl Publishing