LIPIcs, Volume 52
FSCD 2016, June 22-26, 2016, Porto, Portugal
Editors: Delia Kesner and Brigitte Pientka
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Brigitte Pientka. A Modal Analysis of Metaprogramming, Revisited (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{pientka:LIPIcs.FSCD.2020.2, author = {Pientka, Brigitte}, title = {{A Modal Analysis of Metaprogramming, Revisited}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {2:1--2:3}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.2}, URN = {urn:nbn:de:0030-drops-123242}, doi = {10.4230/LIPIcs.FSCD.2020.2}, annote = {Keywords: Type systems, Metaprogramming, Modal Type System} }
Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Rohan Jacob-Rao, Brigitte Pientka, and David Thibodeau. Index-Stratified Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{jacobrao_et_al:LIPIcs.FSCD.2018.19, author = {Jacob-Rao, Rohan and Pientka, Brigitte and Thibodeau, David}, title = {{Index-Stratified Types}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {19:1--19:17}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.19}, URN = {urn:nbn:de:0030-drops-91891}, doi = {10.4230/LIPIcs.FSCD.2018.19}, annote = {Keywords: Indexed types, (co)recursive types, logical relations} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{kaiser_et_al:LIPIcs.FSCD.2017.21, author = {Kaiser, Jonas and Pientka, Brigitte and Smolka, Gert}, title = {{Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {21:1--21:19}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.21}, URN = {urn:nbn:de:0030-drops-77248}, doi = {10.4230/LIPIcs.FSCD.2017.21}, annote = {Keywords: Pure Type Systems, System F, de Bruijn Syntax, Higher-Order Abstract Syntax, Contextual Reasoning} }
Published in: Dagstuhl Reports, Volume 6, Issue 10 (2017)
Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe. Universality of Proofs (Dagstuhl Seminar 16421). In Dagstuhl Reports, Volume 6, Issue 10, pp. 75-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@Article{dowek_et_al:DagRep.6.10.75, author = {Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian}, title = {{Universality of Proofs (Dagstuhl Seminar 16421)}}, pages = {75--98}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2017}, volume = {6}, number = {10}, editor = {Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.10.75}, URN = {urn:nbn:de:0030-drops-69514}, doi = {10.4230/DagRep.6.10.75}, annote = {Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@Proceedings{kesner_et_al:LIPIcs.FSCD.2016, title = {{LIPIcs, Volume 52, FSCD'16, Complete Volume}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016}, URN = {urn:nbn:de:0030-drops-60595}, doi = {10.4230/LIPIcs.FSCD.2016}, annote = {Keywords: Theory of Computation, Computation by abstract devices, Analysis of algorithms and problem complexity, Logics and meanings of programs, Mathematical logic and formal languages, Programming techniques, Software/Program Verification, Programming languages, Deduction and Theorem Proving} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{kesner_et_al:LIPIcs.FSCD.2016.0, author = {Kesner, Delia and Pientka, Brigitte}, title = {{Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {0:i--0:xviii}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.0}, URN = {urn:nbn:de:0030-drops-59672}, doi = {10.4230/LIPIcs.FSCD.2016.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Amal Ahmed. Compositional Compiler Verification for a Multi-Language World. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{ahmed:LIPIcs.FSCD.2016.1, author = {Ahmed, Amal}, title = {{Compositional Compiler Verification for a Multi-Language World}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {1:1--1:1}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.1}, URN = {urn:nbn:de:0030-drops-59680}, doi = {10.4230/LIPIcs.FSCD.2016.1}, annote = {Keywords: verified compilation; compositional compiler correctness, multi-language semantics, typed low-level languages} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Ichiro Hasuo. Coalgebras and Higher-Order Computation: a GoI Approach. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{hasuo:LIPIcs.FSCD.2016.2, author = {Hasuo, Ichiro}, title = {{Coalgebras and Higher-Order Computation: a GoI Approach}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {2:1--2:2}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.2}, URN = {urn:nbn:de:0030-drops-59698}, doi = {10.4230/LIPIcs.FSCD.2016.2}, annote = {Keywords: functional programming, geometry of interaction, categorical semantics, coalgebra} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Gérard Huet. Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{huet:LIPIcs.FSCD.2016.3, author = {Huet, G\'{e}rard}, title = {{Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {3:1--3:2}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.3}, URN = {urn:nbn:de:0030-drops-60020}, doi = {10.4230/LIPIcs.FSCD.2016.3}, annote = {Keywords: Foundations, Computation, Deduction, Programming, Proofs} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Tobias Nipkow. Verified Analysis of Functional Data Structures. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{nipkow:LIPIcs.FSCD.2016.4, author = {Nipkow, Tobias}, title = {{Verified Analysis of Functional Data Structures}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {4:1--4:2}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.4}, URN = {urn:nbn:de:0030-drops-59701}, doi = {10.4230/LIPIcs.FSCD.2016.4}, annote = {Keywords: Program Verification, Algorithm Analysis, Functional Programming} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Ryota Akiyoshi and Kazushige Terui. Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{akiyoshi_et_al:LIPIcs.FSCD.2016.5, author = {Akiyoshi, Ryota and Terui, Kazushige}, title = {{Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {5:1--5:15}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.5}, URN = {urn:nbn:de:0030-drops-59718}, doi = {10.4230/LIPIcs.FSCD.2016.5}, annote = {Keywords: Polymorphic Lambda Calculus, Strong Normalization, Computability Predicate, Infinitary Proof Theory} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2016.6, author = {Altenkirch, Thorsten and Kaposi, Ambrus}, title = {{Normalisation by Evaluation for Dependent Types}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {6:1--6: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.6}, URN = {urn:nbn:de:0030-drops-59727}, doi = {10.4230/LIPIcs.FSCD.2016.6}, annote = {Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Ofer Arieli and Arnon Avron. Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{arieli_et_al:LIPIcs.FSCD.2016.7, author = {Arieli, Ofer and Avron, Arnon}, title = {{Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {7:1--7:15}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.7}, URN = {urn:nbn:de:0030-drops-59731}, doi = {10.4230/LIPIcs.FSCD.2016.7}, annote = {Keywords: Paraconsistecy, Paracompleteness, 4-valued logics} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{arisaka:LIPIcs.FSCD.2016.8, author = {Arisaka, Ryuta}, title = {{Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {8:1--8:18}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.8}, URN = {urn:nbn:de:0030-drops-59742}, doi = {10.4230/LIPIcs.FSCD.2016.8}, annote = {Keywords: cut-elimination, contraction-free, sequent calculus, proof theory, BI, logic combination} }
Feedback for Dagstuhl Publishing