@Proceedings{rehof:LIPIcs.FSCD.2024,
title = {{LIPIcs, Volume 299, FSCD 2024, Complete Volume}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {1--692},
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},
URN = {urn:nbn:de:0030-drops-203287},
doi = {10.4230/LIPIcs.FSCD.2024},
annote = {Keywords: LIPIcs, Volume 299, FSCD 2024, Complete Volume}
}
@InProceedings{rehof:LIPIcs.FSCD.2024.0,
author = {Rehof, Jakob},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {0:i--0:xviii},
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.0},
URN = {urn:nbn:de:0030-drops-203292},
doi = {10.4230/LIPIcs.FSCD.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@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}
}
@InProceedings{cano_et_al:LIPIcs.FSCD.2024.2,
author = {Cano, Filip and Henzinger, Thomas A. and K\"{o}nighofer, Bettina and Kueffner, Konstantin and Mallik, Kaushik},
title = {{Abstraction-Based Decision Making for Statistical Properties}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {2:1--2:17},
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.2},
URN = {urn:nbn:de:0030-drops-203310},
doi = {10.4230/LIPIcs.FSCD.2024.2},
annote = {Keywords: Abstract interpretation, Sequential decision making, Counter machines}
}
@InProceedings{ullrich:LIPIcs.FSCD.2024.3,
author = {Ullrich, Sebastian},
title = {{Lean: Past, Present, and Future}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {3:1--3:2},
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.3},
URN = {urn:nbn:de:0030-drops-203328},
doi = {10.4230/LIPIcs.FSCD.2024.3},
annote = {Keywords: Lean, interactive theorem proving, focused research organization, history}
}
@InProceedings{vanderweide:LIPIcs.FSCD.2024.4,
author = {van der Weide, Niels},
title = {{Univalent Enriched Categories and the Enriched Rezk Completion}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {4:1--4:19},
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.4},
URN = {urn:nbn:de:0030-drops-203337},
doi = {10.4230/LIPIcs.FSCD.2024.4},
annote = {Keywords: enriched categories, univalent categories, homotopy type theory, univalent foundations, Rezk completion}
}
@InProceedings{donato:LIPIcs.FSCD.2024.5,
author = {Donato, Pablo},
title = {{The Flower Calculus}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {5:1--5: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.5},
URN = {urn:nbn:de:0030-drops-203343},
doi = {10.4230/LIPIcs.FSCD.2024.5},
annote = {Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}
@InProceedings{champin_et_al:LIPIcs.FSCD.2024.6,
author = {Champin, Camil and Mimram, Samuel and Oleon, \'{E}mile},
title = {{Delooping Generated Groups in Homotopy Type Theory}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {6:1--6: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.6},
URN = {urn:nbn:de:0030-drops-203356},
doi = {10.4230/LIPIcs.FSCD.2024.6},
annote = {Keywords: homotopy type theory, delooping, group, generator, Cayley graph}
}
@InProceedings{guillemet_et_al:LIPIcs.FSCD.2024.7,
author = {Guillemet, Beno\^{i}t and Mahboubi, Assia and Piquerez, Matthieu},
title = {{Machine-Checked Categorical Diagrammatic Reasoning}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {7:1--7:19},
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.7},
URN = {urn:nbn:de:0030-drops-203363},
doi = {10.4230/LIPIcs.FSCD.2024.7},
annote = {Keywords: Interactive theorem proving, categories, diagrams, formal proof automation}
}
@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}
}
@InProceedings{kerjean_et_al:LIPIcs.FSCD.2024.9,
author = {Kerjean, Marie and Lemay, Jean-Simon Pacaud},
title = {{Laplace Distributors and Laplace Transformations for Differential Categories}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {9:1--9:21},
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.9},
URN = {urn:nbn:de:0030-drops-203382},
doi = {10.4230/LIPIcs.FSCD.2024.9},
annote = {Keywords: Differential Categories, Differential Linear Logic, Laplace Distributor, Laplace Transformation, Exponential Function}
}
@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}
}
@InProceedings{biernacka_et_al:LIPIcs.FSCD.2024.11,
author = {Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan},
title = {{Optimizing a Non-Deterministic Abstract Machine with Environments}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {11:1--11:22},
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.11},
URN = {urn:nbn:de:0030-drops-203409},
doi = {10.4230/LIPIcs.FSCD.2024.11},
annote = {Keywords: Abstract machine, Explicit substitutions, Refocusing}
}
@InProceedings{sannier_et_al:LIPIcs.FSCD.2024.12,
author = {Sannier, Victor and Baillot, Patrick},
title = {{A Linear Type System for L^p-Metric Sensitivity Analysis}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {12:1--12:22},
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.12},
URN = {urn:nbn:de:0030-drops-203412},
doi = {10.4230/LIPIcs.FSCD.2024.12},
annote = {Keywords: type system, linear logic, sensitivity, vector metrics, differential privacy, lambda-calculus, functional programming, denotational semantics}
}
@InProceedings{saito_et_al:LIPIcs.FSCD.2024.13,
author = {Saito, Teppei and Hirokawa, Nao},
title = {{Simulating Dependency Pairs by Semantic Labeling}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {13:1--13: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.13},
URN = {urn:nbn:de:0030-drops-203423},
doi = {10.4230/LIPIcs.FSCD.2024.13},
annote = {Keywords: Term rewriting, Relative termination, Semantic labeling, Dependency pairs}
}
@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
author = {Kavvos, G. A.},
title = {{Two-Dimensional Kripke Semantics I: Presheaves}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {14:1--14: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.14},
URN = {urn:nbn:de:0030-drops-203438},
doi = {10.4230/LIPIcs.FSCD.2024.14},
annote = {Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps}
}
@InProceedings{jang_et_al:LIPIcs.FSCD.2024.15,
author = {Jang, Junyoung and Roshal, Sophia and Pfenning, Frank and Pientka, Brigitte},
title = {{Adjoint Natural Deduction}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {15:1--15: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.15},
URN = {urn:nbn:de:0030-drops-203441},
doi = {10.4230/LIPIcs.FSCD.2024.15},
annote = {Keywords: Substructural Logic, Type Systems, Functional Programming}
}
@InProceedings{baader_et_al:LIPIcs.FSCD.2024.16,
author = {Baader, Franz and Giesl, J\"{u}rgen},
title = {{On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {16:1--16:18},
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.16},
URN = {urn:nbn:de:0030-drops-203454},
doi = {10.4230/LIPIcs.FSCD.2024.16},
annote = {Keywords: Rewriting, Termination, Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting}
}
@InProceedings{gu_et_al:LIPIcs.FSCD.2024.17,
author = {Gu, Tao and Bao, Jialu and Hsu, Justin and Silva, Alexandra and Zanasi, Fabio},
title = {{A Categorical Approach to DIBI Models}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {17:1--17: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.17},
URN = {urn:nbn:de:0030-drops-203469},
doi = {10.4230/LIPIcs.FSCD.2024.17},
annote = {Keywords: Conditional Independence, Dependence Independence Bunched Implications, String Diagrams, Markov Categories}
}
@InProceedings{ito_et_al:LIPIcs.FSCD.2024.18,
author = {Ito, Sohei and Tatsuta, Makoto},
title = {{Representation of Peano Arithmetic in Separation Logic}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {18:1--18:17},
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.18},
URN = {urn:nbn:de:0030-drops-203476},
doi = {10.4230/LIPIcs.FSCD.2024.18},
annote = {Keywords: First order logic, Separation logic, Peano arithmetic, Presburger arithmetic}
}
@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2024.19,
author = {Chardonnet, Kostia and Lemonnier, Louis and Valiron, Beno\^{i}t},
title = {{Semantics for a Turing-Complete Reversible Programming Language with Inductive Types}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {19:1--19:19},
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.19},
URN = {urn:nbn:de:0030-drops-203487},
doi = {10.4230/LIPIcs.FSCD.2024.19},
annote = {Keywords: Reversible programming, functional programming, Computability, Denotational Semantics}
}
@InProceedings{torresruiz_et_al:LIPIcs.FSCD.2024.20,
author = {Torres-Ruiz, Mateo and Piedeleu, Robin and Silva, Alexandra and Zanasi, Fabio},
title = {{On Iteration in Discrete Probabilistic Programming}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {20:1--20:21},
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.20},
URN = {urn:nbn:de:0030-drops-203490},
doi = {10.4230/LIPIcs.FSCD.2024.20},
annote = {Keywords: Probabilistic programming, Programming languages semantics, Unbounded iteration}
}
@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}
}
@InProceedings{dore_et_al:LIPIcs.FSCD.2024.22,
author = {Dor\'{e}, Maximilian and Cavallo, Evan and M\"{o}rtberg, Anders},
title = {{Automating Boundary Filling in Cubical Agda}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {22:1--22:18},
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.22},
URN = {urn:nbn:de:0030-drops-203514},
doi = {10.4230/LIPIcs.FSCD.2024.22},
annote = {Keywords: Cubical Agda, Automated Reasoning, Constraint Satisfaction Programming}
}
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23,
author = {Accattoli, Beniamino and Lancelot, Adrienne},
title = {{Mirroring Call-By-Need, or Values Acting Silly}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {23:1--23: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.23},
URN = {urn:nbn:de:0030-drops-203527},
doi = {10.4230/LIPIcs.FSCD.2024.23},
annote = {Keywords: Lambda calculus, intersection types, call-by-value, call-by-need}
}
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24,
author = {Accattoli, Beniamino and Sacerdoti Coen, Claudio},
title = {{IMELL Cut Elimination with Linear Overhead}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {24:1--24: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.24},
URN = {urn:nbn:de:0030-drops-203539},
doi = {10.4230/LIPIcs.FSCD.2024.24},
annote = {Keywords: Lambda calculus, linear logic, abstract machines}
}
@InProceedings{matthes_et_al:LIPIcs.FSCD.2024.25,
author = {Matthes, Ralph and Wullaert, Kobe and Ahrens, Benedikt},
title = {{Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {25:1--25:22},
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.25},
URN = {urn:nbn:de:0030-drops-203540},
doi = {10.4230/LIPIcs.FSCD.2024.25},
annote = {Keywords: Non-wellfounded syntax, Substitution, Monoidal categories, Actegories, Tensorial strength, Proof assistant Coq, UniMath library}
}
@InProceedings{herbelin_et_al:LIPIcs.FSCD.2024.26,
author = {Herbelin, Hugo and Koleilat, Jad},
title = {{On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {26:1--26:15},
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.26},
URN = {urn:nbn:de:0030-drops-203551},
doi = {10.4230/LIPIcs.FSCD.2024.26},
annote = {Keywords: axiom of choice, Teichm\"{u}ller-Tukey lemma, update induction, constructive reverse mathematics}
}
@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27,
author = {Thiemann, Ren\'{e} and Yamada, Akihisa},
title = {{A Verified Algorithm for Deciding Pattern Completeness}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {27:1--27:17},
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.27},
URN = {urn:nbn:de:0030-drops-203566},
doi = {10.4230/LIPIcs.FSCD.2024.27},
annote = {Keywords: Isabelle/HOL, pattern matching, term rewriting}
}
@InProceedings{abramsky_et_al:LIPIcs.FSCD.2024.28,
author = {Abramsky, Samson and Cercelescu, \c{S}erban-Ion and Constantin, Carmen-Maria},
title = {{Commutation Groups and State-Independent Contextuality}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {28:1--28: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.28},
URN = {urn:nbn:de:0030-drops-203572},
doi = {10.4230/LIPIcs.FSCD.2024.28},
annote = {Keywords: Contextuality, state-independence, quantum mechanics, Pauli group, group presentations, unitary representations}
}
@InProceedings{dufour_et_al:LIPIcs.FSCD.2024.29,
author = {Dufour, Alo\"{y}s and Mazza, Damiano},
title = {{B\"{o}hm and Taylor for All!}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {29:1--29: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.29},
URN = {urn:nbn:de:0030-drops-203582},
doi = {10.4230/LIPIcs.FSCD.2024.29},
annote = {Keywords: Linear logic, Differential linear logic, Taylor expansion of lambda-terms, B\"{o}hm trees, Process calculi}
}
@InProceedings{corbyn_et_al:LIPIcs.FSCD.2024.30,
author = {Corbyn, Nathan and Heidemann, Lukas and Hu, Nick and Sarti, Chiara and Tataru, Calin and Vicary, Jamie},
title = {{homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {30:1--30:26},
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.30},
URN = {urn:nbn:de:0030-drops-203594},
doi = {10.4230/LIPIcs.FSCD.2024.30},
annote = {Keywords: Higher category theory, proof assistant, string diagrams}
}
@InProceedings{aoto_et_al:LIPIcs.FSCD.2024.31,
author = {Aoto, Takahito and Nishida, Naoki and Sch\"{o}pf, Jonas},
title = {{Equational Theories and Validity for Logically Constrained Term Rewriting}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {31:1--31:21},
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.31},
URN = {urn:nbn:de:0030-drops-203607},
doi = {10.4230/LIPIcs.FSCD.2024.31},
annote = {Keywords: constrained equation, constrained equational theory, logically constrained term rewriting, algebraic semantics, consistency}
}
@InProceedings{lucas:LIPIcs.FSCD.2024.32,
author = {Lucas, Salvador},
title = {{Termination of Generalized Term Rewriting Systems}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {32:1--32:18},
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.32},
URN = {urn:nbn:de:0030-drops-203616},
doi = {10.4230/LIPIcs.FSCD.2024.32},
annote = {Keywords: Program Analysis, Reduction-Based Systems, Termination}
}
@InProceedings{deoliveiraoliveira_et_al:LIPIcs.FSCD.2024.33,
author = {de Oliveira Oliveira, Mateus and Vadiee, Farhad},
title = {{State Canonization and Early Pruning in Width-Based Automated Theorem Proving}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {33:1--33:17},
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.33},
URN = {urn:nbn:de:0030-drops-203622},
doi = {10.4230/LIPIcs.FSCD.2024.33},
annote = {Keywords: Width-Based Automated Theorem Proving, Dynamic Programming, Parameterized Complexity}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing