Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Andrew M. Pitts. Quotients in Dependent Type Theory (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{pitts:LIPIcs.FSCD.2020.3, author = {Pitts, Andrew M.}, title = {{Quotients in Dependent Type Theory}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {3:1--3:2}, 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.3}, URN = {urn:nbn:de:0030-drops-123256}, doi = {10.4230/LIPIcs.FSCD.2020.3}, annote = {Keywords: dependent type theory, quotient, quotient inductive type, theorem-proving systems} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1, author = {Berger, Ulrich and Matthes, Ralph and Setzer, Anton}, title = {{Martin Hofmann’s Case for Non-Strictly Positive Data Types}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {1:1--1:22}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1}, URN = {urn:nbn:de:0030-drops-114052}, doi = {10.4230/LIPIcs.TYPES.2018.1}, annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell} }
Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)
Andrej Bauer, Martin Hofmann, Matija Pretnar, and Jeremy Yallop. From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112). In Dagstuhl Reports, Volume 6, Issue 3, pp. 44-58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@Article{bauer_et_al:DagRep.6.3.44, author = {Bauer, Andrej and Hofmann, Martin and Pretnar, Matija and Yallop, Jeremy}, title = {{From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112)}}, pages = {44--58}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2016}, volume = {6}, number = {3}, editor = {Bauer, Andrej and Hofmann, Martin and Pretnar, Matija and Yallop, Jeremy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.3.44}, URN = {urn:nbn:de:0030-drops-61489}, doi = {10.4230/DagRep.6.3.44}, annote = {Keywords: algebraic effects, computational effects, handlers, implementation techniques, programming languages} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Martin Hofmann and Georg Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 241-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hofmann_et_al:LIPIcs.TLCA.2015.241, author = {Hofmann, Martin and Moser, Georg}, title = {{Multivariate Amortised Resource Analysis for Term Rewrite Systems}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {241--256}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.241}, URN = {urn:nbn:de:0030-drops-51675}, doi = {10.4230/LIPIcs.TLCA.2015.241}, annote = {Keywords: program analysis,amortised analysis, term rewriting,multivariate bounds} }
Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)
Martin Hofmann and Ramyaa Ramyaa. Computing With a Fixed Number of Pointers (Invited Talk). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 3-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{hofmann_et_al:LIPIcs.FSTTCS.2013.3, author = {Hofmann, Martin and Ramyaa, Ramyaa}, title = {{Computing With a Fixed Number of Pointers}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)}, pages = {3--18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-64-4}, ISSN = {1868-8969}, year = {2013}, volume = {24}, editor = {Seth, Anil and Vishnoi, Nisheeth K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.3}, URN = {urn:nbn:de:0030-drops-44009}, doi = {10.4230/LIPIcs.FSTTCS.2013.3}, annote = {Keywords: Logarithmic space, Jumping graph automata, st-connectivity, co-st-connectivity, Cayley graphs} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Abstracts Collection – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{ahmed_et_al:DagSemProc.10351.1, author = {Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin}, title = {{10351 Abstracts Collection – Modelling, Controlling and Reasoning About State}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--16}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.1}, URN = {urn:nbn:de:0030-drops-28116}, doi = {10.4230/DagSemProc.10351.1}, annote = {Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Executive Summary – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{ahmed_et_al:DagSemProc.10351.2, author = {Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin}, title = {{10351 Executive Summary – Modelling, Controlling and Reasoning About State}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--4}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.2}, URN = {urn:nbn:de:0030-drops-28108}, doi = {10.4230/DagSemProc.10351.2}, annote = {Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Robert Dockins and Aquinas Hobor. A Theory of Termination via Indirection. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{dockins_et_al:DagSemProc.10351.3, author = {Dockins, Robert and Hobor, Aquinas}, title = {{A Theory of Termination via Indirection}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--12}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.3}, URN = {urn:nbn:de:0030-drops-28050}, doi = {10.4230/DagSemProc.10351.3}, annote = {Keywords: Step-indexed Models, Termination} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{koutavas_et_al:DagSemProc.10351.4, author = {Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro}, title = {{Limitations of Applicative Bisimulation (Preliminary Report)}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--9}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.4}, URN = {urn:nbn:de:0030-drops-28074}, doi = {10.4230/DagSemProc.10351.4}, annote = {Keywords: Imperative languages, higher-order functions, local state} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Nikos Tzevelekos. Program Equivalence with Names. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{tzevelekos:DagSemProc.10351.5, author = {Tzevelekos, Nikos}, title = {{Program Equivalence with Names}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--18}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.5}, URN = {urn:nbn:de:0030-drops-28092}, doi = {10.4230/DagSemProc.10351.5}, annote = {Keywords: Nu-calculus, Local State, Logical Relations, Game Semantics, Environmental Bisimulations} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Andrew M. Pitts. Step-Indexed Biorthogonality: a Tutorial Example. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{pitts:DagSemProc.10351.6, author = {Pitts, Andrew M.}, title = {{Step-Indexed Biorthogonality: a Tutorial Example}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--10}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.6}, URN = {urn:nbn:de:0030-drops-28067}, doi = {10.4230/DagSemProc.10351.6}, annote = {Keywords: Biorthogonality, logical relations, operational semantics, step-indexing} }
Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)
Nick Benton and Chung-Kil Hur. Step-Indexing: The Good, the Bad and the Ugly. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{benton_et_al:DagSemProc.10351.7, author = {Benton, Nick and Hur, Chung-Kil}, title = {{Step-Indexing: The Good, the Bad and the Ugly}}, booktitle = {Modelling, Controlling and Reasoning About State}, pages = {1--9}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10351}, editor = {Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.7}, URN = {urn:nbn:de:0030-drops-28085}, doi = {10.4230/DagSemProc.10351.7}, annote = {Keywords: Step-Indexing, Logical Relations, Low-Level Languages, Compiler Correctness} }
Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)
Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett. 08061 Abstracts Collection – Types, Logics and Semantics for State. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)
@InProceedings{ahmed_et_al:DagSemProc.08061.1, author = {Ahmed, Amal and Benton, Nick and Hofmann, Martin and Morrisett, Greg}, title = {{08061 Abstracts Collection – Types, Logics and Semantics for State}}, booktitle = {Types, Logics and Semantics for State}, pages = {1--20}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2008}, volume = {8061}, editor = {Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.1}, URN = {urn:nbn:de:0030-drops-14281}, doi = {10.4230/DagSemProc.08061.1}, annote = {Keywords: Mutable State, Program Logics, Semantics, Type Systems, Program Analysis} }
Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)
Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett. 08061 Executive Summary – Types, Logics and Semantics for State. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)
@InProceedings{ahmed_et_al:DagSemProc.08061.2, author = {Ahmed, Amal and Benton, Nick and Hofmann, Martin and Morrisett, Greg}, title = {{08061 Executive Summary – Types, Logics and Semantics for State}}, booktitle = {Types, Logics and Semantics for State}, pages = {1--3}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2008}, volume = {8061}, editor = {Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.2}, URN = {urn:nbn:de:0030-drops-14269}, doi = {10.4230/DagSemProc.08061.2}, annote = {Keywords: Mutable State, Program Logics, Semantics, Type Systems, Program Analysis} }
Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)
Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers. A Unified Framework for Verification Techniques for Object Invariants. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)
@InProceedings{drossopoulou_et_al:DagSemProc.08061.3, author = {Drossopoulou, Sophia and Francalanza, Adrian and M\"{u}ller, P. and Summers, Alexander J.}, title = {{A Unified Framework for Verification Techniques for Object Invariants}}, booktitle = {Types, Logics and Semantics for State}, pages = {1--25}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2008}, volume = {8061}, editor = {Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.3}, URN = {urn:nbn:de:0030-drops-14278}, doi = {10.4230/DagSemProc.08061.3}, annote = {Keywords: Object invariants, visible states semantics, verification, sound} }
Feedback for Dagstuhl Publishing