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.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 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 12:1-12:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{takahashi:LIPIcs.TYPES.2021.12, author = {Takahashi, Yuta}, title = {{Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {12:1--12:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.12}, URN = {urn:nbn:de:0030-drops-167811}, doi = {10.4230/LIPIcs.TYPES.2021.12}, annote = {Keywords: termination, higher-order rewriting, non-positive types, inductive types} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Frédéric Blanqui. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 24:1-24:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{blanqui:LIPIcs.FSCD.2022.24, author = {Blanqui, Fr\'{e}d\'{e}ric}, title = {{Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {24:1--24:14}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.24}, URN = {urn:nbn:de:0030-drops-163059}, doi = {10.4230/LIPIcs.FSCD.2022.24}, annote = {Keywords: logical framework, type theory, type universes, rewriting} }
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.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.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.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 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Frédéric Blanqui. Type Safety of Rewrite Rules in Dependent Types. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 13:1-13:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{blanqui:LIPIcs.FSCD.2020.13, author = {Blanqui, Fr\'{e}d\'{e}ric}, title = {{Type Safety of Rewrite Rules in Dependent Types}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {13:1--13:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.13}, URN = {urn:nbn:de:0030-drops-123353}, doi = {10.4230/LIPIcs.FSCD.2020.13}, annote = {Keywords: subject-reduction, rewriting, dependent types} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Guillaume Genestier. Encoding Agda Programs Using Rewriting. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 31:1-31:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{genestier:LIPIcs.FSCD.2020.31, author = {Genestier, Guillaume}, title = {{Encoding Agda Programs Using Rewriting}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {31:1--31:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.31}, URN = {urn:nbn:de:0030-drops-123530}, doi = {10.4230/LIPIcs.FSCD.2020.31}, annote = {Keywords: Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 35:1-35:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{hondet_et_al:LIPIcs.FSCD.2020.35, author = {Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric}, title = {{The New Rewriting Engine of Dedukti}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {35:1--35:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.35}, URN = {urn:nbn:de:0030-drops-123577}, doi = {10.4230/LIPIcs.FSCD.2020.35}, annote = {Keywords: rewriting, higher-order pattern-matching, decision trees} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 9:1-9:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{blanqui_et_al:LIPIcs.FSCD.2019.9, author = {Blanqui, Fr\'{e}d\'{e}ric and Genestier, Guillaume and Hermant, Olivier}, title = {{Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {9:1--9:21}, 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.9}, URN = {urn:nbn:de:0030-drops-105167}, doi = {10.4230/LIPIcs.FSCD.2019.9}, annote = {Keywords: termination, higher-order rewriting, dependent types, dependency pairs} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Ali Assaf. Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 31-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{assaf:LIPIcs.TLCA.2015.31, author = {Assaf, Ali}, title = {{Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {31--44}, 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.31}, URN = {urn:nbn:de:0030-drops-51535}, doi = {10.4230/LIPIcs.TLCA.2015.31}, annote = {Keywords: lambda Pi calculus modulo rewriting, pure type systems, logical framework, normalization, conservativit} }
Feedback for Dagstuhl Publishing