Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{clune_et_al:LIPIcs.ITP.2024.10, author = {Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy}, title = {{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {10:1--10:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10}, URN = {urn:nbn:de:0030-drops-207381}, doi = {10.4230/LIPIcs.ITP.2024.10}, annote = {Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Andrej Dudenhefner, Christoph Stahl, Constantin Chaumet, Felix Laarmann, and Jakob Rehof. Finite Combinatory Logic with Predicates. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 2:1-2:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2023.2, author = {Dudenhefner, Andrej and Stahl, Christoph and Chaumet, Constantin and Laarmann, Felix and Rehof, Jakob}, title = {{Finite Combinatory Logic with Predicates}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {2:1--2:22}, 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.2}, URN = {urn:nbn:de:0030-drops-204808}, doi = {10.4230/LIPIcs.TYPES.2023.2}, annote = {Keywords: combinatory logic, inhabitation, intersection types, program synthesis} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{krebbers:LIPIcs.ITP.2023.2, author = {Krebbers, Robbert}, title = {{Interactive and Automated Proofs in Modal Separation Logic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2}, URN = {urn:nbn:de:0030-drops-183770}, doi = {10.4230/LIPIcs.ITP.2023.2}, annote = {Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting Tree Grammars with Term Rewriting. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{bessai_et_al:LIPIcs.FSCD.2022.14, author = {Bessai, Jan and Czajka, Lukasz and Laarmann, Felix and Rehof, Jakob}, title = {{Restricting Tree Grammars with Term Rewriting}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {14:1--14:19}, 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.14}, URN = {urn:nbn:de:0030-drops-162953}, doi = {10.4230/LIPIcs.FSCD.2022.14}, annote = {Keywords: tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Łukasz Czajka. First-Order Guarded Coinduction in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{czajka:LIPIcs.ITP.2019.14, author = {Czajka, {\L}ukasz}, title = {{First-Order Guarded Coinduction in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {14:1--14:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.14}, URN = {urn:nbn:de:0030-drops-110690}, doi = {10.4230/LIPIcs.ITP.2019.14}, annote = {Keywords: coinduction, Coq, guardedness, corecursion} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Łukasz Czajka and Cynthia Kop. Polymorphic Higher-Order Termination. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{czajka_et_al:LIPIcs.FSCD.2019.12, author = {Czajka, {\L}ukasz and Kop, Cynthia}, title = {{Polymorphic Higher-Order Termination}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {12:1--12:18}, 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.12}, URN = {urn:nbn:de:0030-drops-105193}, doi = {10.4230/LIPIcs.FSCD.2019.12}, annote = {Keywords: termination, polymorphism, higher-order rewriting, permutative conversions} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Lukasz Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 9:1-9:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{czajka:LIPIcs.TYPES.2016.9, author = {Czajka, Lukasz}, title = {{A Shallow Embedding of Pure Type Systems into First-Order Logic}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {9:1--9:39}, 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.9}, URN = {urn:nbn:de:0030-drops-98533}, doi = {10.4230/LIPIcs.TYPES.2016.9}, annote = {Keywords: pure type systems, first-order logic, hammers, proof automation, dependent type theory} }
Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Lukasz Czajka. Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{czajka:LIPIcs.FSCD.2018.13, author = {Czajka, Lukasz}, title = {{Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {13:1--13:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.13}, URN = {urn:nbn:de:0030-drops-91831}, doi = {10.4230/LIPIcs.FSCD.2018.13}, annote = {Keywords: LOGSPACE, implicit complexity, term rewriting, infinitary rewriting, streams} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Lukasz Czajka. Confluence of an Extension of Combinatory Logic by Boolean Constants. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{czajka:LIPIcs.FSCD.2017.14, author = {Czajka, Lukasz}, title = {{Confluence of an Extension of Combinatory Logic by Boolean Constants}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {14:1--14:16}, 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.14}, URN = {urn:nbn:de:0030-drops-77368}, doi = {10.4230/LIPIcs.FSCD.2017.14}, annote = {Keywords: combinatory logic, conditional linearization, unique normal form property, confluence} }
Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Lukasz Czajka. Confluence of nearly orthogonal infinitary term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 106-126, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{czajka:LIPIcs.RTA.2015.106, author = {Czajka, Lukasz}, title = {{Confluence of nearly orthogonal infinitary term rewriting systems}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {106--126}, 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.106}, URN = {urn:nbn:de:0030-drops-51929}, doi = {10.4230/LIPIcs.RTA.2015.106}, annote = {Keywords: infinitary rewriting, confluence, coinduction} }
Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)
Lukasz Czajka. A Semantic Approach to Illative Combinatory Logic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 174-188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
@InProceedings{czajka:LIPIcs.CSL.2011.174, author = {Czajka, Lukasz}, title = {{A Semantic Approach to Illative Combinatory Logic}}, booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL}, pages = {174--188}, 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.174}, URN = {urn:nbn:de:0030-drops-32303}, doi = {10.4230/LIPIcs.CSL.2011.174}, annote = {Keywords: illative combinatory logic, term rewriting, first-order logic} }
Feedback for Dagstuhl Publishing