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 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Andrej Dudenhefner and Daniele Pautasso. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2024.8, author = {Dudenhefner, Andrej and Pautasso, Daniele}, title = {{Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {8:1--8:20}, 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.8}, URN = {urn:nbn:de:0030-drops-203371}, doi = {10.4230/LIPIcs.FSCD.2024.8}, annote = {Keywords: lambda-calculus, simple types, intersection types, strong normalization, mechanization, perpetual reductions} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Delia Kesner, Delia Kesner, Victor Arrial, Victor Arrial, Giulio Guerrieri, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kesner_et_al:LIPIcs.FSCD.2024.1, author = {Kesner, Delia and Arrial, Victor and Guerrieri, Giulio}, title = {{Meaningfulness and Genericity in a Subsuming Framework}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {1:1--1: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.1}, URN = {urn:nbn:de:0030-drops-203305}, doi = {10.4230/LIPIcs.FSCD.2024.1}, annote = {Keywords: Lambda calculus, Solvability, Meaningfulness, Inhabitation, Genericity} }
Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{forster_et_al:LIPIcs.CSL.2023.21, author = {Forster, Yannick and Jahn, Felix}, title = {{Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {21:1--21:21}, 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.21}, URN = {urn:nbn:de:0030-drops-174820}, doi = {10.4230/LIPIcs.CSL.2023.21}, annote = {Keywords: type theory, computability theory, constructive mathematics, Coq} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of Dyadic First-Order Logic in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{hostert_et_al:LIPIcs.ITP.2022.19, author = {Hostert, Johannes and Dudenhefner, Andrej and Kirst, Dominik}, title = {{Undecidability of Dyadic First-Order Logic in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {19:1--19:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.19}, URN = {urn:nbn:de:0030-drops-167280}, doi = {10.4230/LIPIcs.ITP.2022.19}, annote = {Keywords: undecidability, synthetic computability, first-order logic, Coq} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Andrej Dudenhefner. Certified Decision Procedures for Two-Counter Machines. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dudenhefner:LIPIcs.FSCD.2022.16, author = {Dudenhefner, Andrej}, title = {{Certified Decision Procedures for Two-Counter Machines}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {16:1--16: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.16}, URN = {urn:nbn:de:0030-drops-162978}, doi = {10.4230/LIPIcs.FSCD.2022.16}, annote = {Keywords: constructive mathematics, computability theory, decidability, counter automata, mechanization, Coq} }
Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Andrej Dudenhefner. Constructive Many-One Reduction from the Halting Problem to Semi-Unification. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dudenhefner:LIPIcs.CSL.2022.18, author = {Dudenhefner, Andrej}, title = {{Constructive Many-One Reduction from the Halting Problem to Semi-Unification}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {18:1--18:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.18}, URN = {urn:nbn:de:0030-drops-157380}, doi = {10.4230/LIPIcs.CSL.2022.18}, annote = {Keywords: constructive mathematics, undecidability, mechanization, semi-unification} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{kirst_et_al:LIPIcs.ITP.2021.23, author = {Kirst, Dominik and Hermes, Marc}, title = {{Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {23:1--23:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.23}, URN = {urn:nbn:de:0030-drops-139188}, doi = {10.4230/LIPIcs.ITP.2021.23}, annote = {Keywords: undecidability, synthetic computability, first-order logic, incompleteness, Peano arithmetic, ZF set theory, constructive type theory, Coq} }
Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{forster:LIPIcs.CSL.2021.21, author = {Forster, Yannick}, title = {{Church’s Thesis and Related Axioms in Coq’s Type Theory}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {21:1--21:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.21}, URN = {urn:nbn:de:0030-drops-134552}, doi = {10.4230/LIPIcs.CSL.2021.21}, annote = {Keywords: Church’s thesis, constructive type theory, constructive reverse mathematics, synthetic computability theory, Coq} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Andrej Dudenhefner. Undecidability of Semi-Unification on a Napkin. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{dudenhefner:LIPIcs.FSCD.2020.9, author = {Dudenhefner, Andrej}, title = {{Undecidability of Semi-Unification on a Napkin}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {9:1--9: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.9}, URN = {urn:nbn:de:0030-drops-123311}, doi = {10.4230/LIPIcs.FSCD.2020.9}, annote = {Keywords: undecidability, semi-unification, mechanization} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2, author = {Dudenhefner, Andrej and Rehof, Jakob}, title = {{A Simpler Undecidability Proof for System F Inhabitation}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {2:1--2:11}, 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.2}, URN = {urn:nbn:de:0030-drops-114061}, doi = {10.4230/LIPIcs.TYPES.2018.2}, annote = {Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2017.2, author = {Dudenhefner, Andrej and Rehof, Jakob}, title = {{Lower End of the Linial-Post Spectrum}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {2:1--2:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.2}, URN = {urn:nbn:de:0030-drops-100503}, doi = {10.4230/LIPIcs.TYPES.2017.2}, annote = {Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Andrej Dudenhefner and Jakob Rehof. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2017.15, author = {Dudenhefner, Andrej and Rehof, Jakob}, title = {{The Complexity of Principal Inhabitation}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {15:1--15:14}, 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.15}, URN = {urn:nbn:de:0030-drops-77359}, doi = {10.4230/LIPIcs.FSCD.2017.15}, annote = {Keywords: Lambda Calculus, Type Theory, Simple Types, Inhabitation, Principal Type, Complexity} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The Intersection Type Unification Problem. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2016.19, author = {Dudenhefner, Andrej and Martens, Moritz and Rehof, Jakob}, title = {{The Intersection Type Unification Problem}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {19:1--19:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, year = {2016}, volume = {52}, editor = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.19}, URN = {urn:nbn:de:0030-drops-59955}, doi = {10.4230/LIPIcs.FSCD.2016.19}, annote = {Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof. Mixin Composition Synthesis Based on Intersection Types. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 76-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{bessai_et_al:LIPIcs.TLCA.2015.76, author = {Bessai, Jan and Dudenhefner, Andrej and D\"{u}dder, Boris and Chen, Tzu-Chun and de’Liguoro, Ugo and Rehof, Jakob}, title = {{Mixin Composition Synthesis Based on Intersection Types}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {76--91}, 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.76}, URN = {urn:nbn:de:0030-drops-51563}, doi = {10.4230/LIPIcs.TLCA.2015.76}, annote = {Keywords: Record Calculus, Combinatory Logic, Type Inhabitation, Mixin, Intersection Type} }
Feedback for Dagstuhl Publishing