LIPIcs, Volume 228
FSCD 2022, August 2-5, 2022, Haifa, Israel
Editors: Amy P. Felty
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Amy Felty. Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{felty:LIPIcs.ITP.2022.1, author = {Felty, Amy}, title = {{Modelling and Verifying Properties of Biological Neural Networks}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {1:1--1:2}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.1}, URN = {urn:nbn:de:0030-drops-167100}, doi = {10.4230/LIPIcs.ITP.2022.1}, annote = {Keywords: Neuronal networks, Model checking, Theorem proving, Coq} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 1-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@Proceedings{felty:LIPIcs.FSCD.2022, title = {{LIPIcs, Volume 228, FSCD 2022, Complete Volume}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {1--652}, 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}, URN = {urn:nbn:de:0030-drops-162803}, doi = {10.4230/LIPIcs.FSCD.2022}, annote = {Keywords: LIPIcs, Volume 228, FSCD 2022, Complete Volume} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{felty:LIPIcs.FSCD.2022.0, author = {Felty, Amy P.}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {0:i--0:xviii}, 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.0}, URN = {urn:nbn:de:0030-drops-162814}, doi = {10.4230/LIPIcs.FSCD.2022.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Cynthia Kop. Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{kop:LIPIcs.FSCD.2022.1, author = {Kop, Cynthia}, title = {{Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {1:1--1: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.1}, URN = {urn:nbn:de:0030-drops-162827}, doi = {10.4230/LIPIcs.FSCD.2022.1}, annote = {Keywords: Termination, Modularity, Higher-order term rewriting, Dependency Pairs, Algebra Interpretations} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Alwen Tiu. A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 2:1-2:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{tiu:LIPIcs.FSCD.2022.2, author = {Tiu, Alwen}, title = {{A Methodology for Designing Proof Search Calculi for Non-Classical Logics}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {2:1--2:4}, 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.2}, URN = {urn:nbn:de:0030-drops-162834}, doi = {10.4230/LIPIcs.FSCD.2022.2}, annote = {Keywords: Proof theory, Sequent calculus, Display calculus, Nested sequent calculus, Deep inference} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Francesco Dagnino and Francesco Gavazzo. A Fibrational Tale of Operational Logical Relations. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dagnino_et_al:LIPIcs.FSCD.2022.3, author = {Dagnino, Francesco and Gavazzo, Francesco}, title = {{A Fibrational Tale of Operational Logical Relations}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {3:1--3:21}, 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.3}, URN = {urn:nbn:de:0030-drops-162840}, doi = {10.4230/LIPIcs.FSCD.2022.3}, annote = {Keywords: logical relations, operational semantics, fibrations, generic effects, program distance} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dallago_et_al:LIPIcs.FSCD.2022.4, author = {Dal Lago, Ugo and Honsell, Furio and Lenisa, Marina and Pistone, Paolo}, title = {{On Quantitative Algebraic Higher-Order Theories}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {4:1--4: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.4}, URN = {urn:nbn:de:0030-drops-162851}, doi = {10.4230/LIPIcs.FSCD.2022.4}, annote = {Keywords: Quantitative Algebras, Lambda Calculus, Combinatory Logic, Metric Spaces} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{sterling_et_al:LIPIcs.FSCD.2022.5, author = {Sterling, Jonathan and Harper, Robert}, title = {{Sheaf Semantics of Termination-Insensitive Noninterference}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {5:1--5: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.5}, URN = {urn:nbn:de:0030-drops-162869}, doi = {10.4230/LIPIcs.FSCD.2022.5}, annote = {Keywords: information flow, noninterference, denotational semantics, phase distinction, Artin gluing, modal type theory, topos theory, synthetic domain theory, synthetic Tait computability} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Combined Hierarchical Matching: the Regular Case. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{erbatur_et_al:LIPIcs.FSCD.2022.6, author = {Erbatur, Serdar and Marshall, Andrew M. and Ringeissen, Christophe}, title = {{Combined Hierarchical Matching: the Regular Case}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {6:1--6:22}, 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.6}, URN = {urn:nbn:de:0030-drops-162879}, doi = {10.4230/LIPIcs.FSCD.2022.6}, annote = {Keywords: Matching, combination problem, equational theories} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho. Nominal Anti-Unification with Atom-Variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2022.7, author = {Schmidt-Schau{\ss}, Manfred and Nantes-Sobrinho, Daniele}, title = {{Nominal Anti-Unification with Atom-Variables}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {7:1--7:22}, 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.7}, URN = {urn:nbn:de:0030-drops-162885}, doi = {10.4230/LIPIcs.FSCD.2022.7}, annote = {Keywords: Generalization, anti-unification, nominal algorithms, higher-order deduction} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes Sobrinho. A Certified Algorithm for AC-Unification. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2022.8, author = {Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Silva, Gabriel Ferreira and Sobrinho, Daniele Nantes}, title = {{A Certified Algorithm for AC-Unification}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {8:1--8:21}, 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.8}, URN = {urn:nbn:de:0030-drops-162894}, doi = {10.4230/LIPIcs.FSCD.2022.8}, annote = {Keywords: AC-Unification, PVS, Certified Algorithms, Formal Methods, Interactive Theorem Proving} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Marc Hermes and Dominik Kirst. An Analysis of Tennenbaum’s Theorem in Constructive Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{hermes_et_al:LIPIcs.FSCD.2022.9, author = {Hermes, Marc and Kirst, Dominik}, title = {{An Analysis of Tennenbaum’s Theorem in Constructive Type Theory}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {9:1--9: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.9}, URN = {urn:nbn:de:0030-drops-162909}, doi = {10.4230/LIPIcs.FSCD.2022.9}, annote = {Keywords: first-order logic, Peano arithmetic, Tennenbaum’s theorem, constructive type theory, Church’s thesis, synthetic computability, Coq} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Liron Cohen and Vincent Rahli. Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{cohen_et_al:LIPIcs.FSCD.2022.10, author = {Cohen, Liron and Rahli, Vincent}, title = {{Constructing Unprejudiced Extensional Type Theories with Choices via Modalities}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {10:1--10:23}, 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.10}, URN = {urn:nbn:de:0030-drops-162917}, doi = {10.4230/LIPIcs.FSCD.2022.10}, annote = {Keywords: Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Choice sequences, References, Classical Logic, Theorem proving, Agda} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Samuel Mimram and Émile Oleon. Division by Two, in Homotopy Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{mimram_et_al:LIPIcs.FSCD.2022.11, author = {Mimram, Samuel and Oleon, \'{E}mile}, title = {{Division by Two, in Homotopy Type Theory}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {11:1--11: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.11}, URN = {urn:nbn:de:0030-drops-162920}, doi = {10.4230/LIPIcs.FSCD.2022.11}, annote = {Keywords: division, axiom of choice, set theory, homotopy type theory, Agda} }
Feedback for Dagstuhl Publishing