Search Results

Documents authored by Hofmann, Martin

Document
DOI: 10.4230/DagRep.6.3.44
From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112)

Authors: Andrej Bauer, Martin Hofmann, Matija Pretnar, and Jeremy Yallop

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)

Abstract
Dagstuhl Seminar 16112 was devoted to research in algebraic effects and handlers, a chapter in the principles of programming languages which addresses computational effects (such as I/O, state, exceptions, nondeterminism, and many others). The speakers and the working groups covered a range of topics, including comparisons between various control mechanisms (handlers vs. delimited control), implementation of an effect system for OCaml, compilation techniques for algebraic effects and handlers, and implementations of effects in Haskell.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.241
Multivariate Amortised Resource Analysis for Term Rewrite Systems

Authors: Martin Hofmann and Georg Moser

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
We study amortised resource analysis in the context of term rewrite systems. We introduce a novel amortised analysis based on the potential method. The method is represented in an inference system akin to a type system and gives rise to polynomial bounds on the innermost runtime complexity of the analysed rewrite system. The crucial feature of the inference system is the admittance of multivariate bounds in the context of arbitrary data structures in a completely uniform way. This extends our earlier univariate resource analysis of typed term rewrite systems and continues our program of applying automated amortised resource analysis to rewriting.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2013.3
Computing With a Fixed Number of Pointers (Invited Talk)

Authors: Martin Hofmann and Ramyaa Ramyaa

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
Consider the P-complete problem Horn which asks whether a given set of Horn clauses is (un)satisfiable. To solve it one keeps a dynamic set of atoms that are forced to be true. Using the clauses one then adds atoms to this set until saturation is reached. It is easy to see that this dynamic set will in general more than constant size even if we allow to discard already proved atoms. Given that we need logarithmic space to store a single atom on a Turing machine tape this seems like a strong intuitive argument for the hypothesis that logarithmic space is different from polynomial time. We thus tried to find formal models of computation in which this intuitive argument can be made rigorous. Thus, we study computational models that can be simulated in logarithmic space and encompass logspace algorithms which manipulate a constant size of objects that require logarithmic space individually such as pointers or graph nodes. The hope is then to be able to show that such models are provably unable to solve P-complete problems. We report in this survey article on our partial results towards this goal as well as the state-of-the-art in general.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/DagSemProc.10351.1
10351 Abstracts Collection – Modelling, Controlling and Reasoning About State

Authors: Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351 ``Modelling, Controlling and Reasoning About State '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. Links to extended abstracts or full papers are provided, if available.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/DagSemProc.10351.2
10351 Executive Summary – Modelling, Controlling and Reasoning About State

Authors: Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351 ``Modelling, Controlling and Reasoning About State '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. 44 researchers, with interests and expertise in many different aspects of modelling and reasoning about mutable state, met to present their current work and discuss ongoing projects and open problems. This executive summary provides a general overview of the goals of the seminar and of the topics discussed.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/DagSemProc.08061.1
08061 Abstracts Collection – Types, Logics and Semantics for State

Authors: Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)

Abstract
From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 ``Types, Logics and Semantics for State'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/DagSemProc.08061.2
08061 Executive Summary – Types, Logics and Semantics for State

Authors: Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)

Abstract
From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 State" Conference and Research Center (IBFI), Schloss Dagstuhl. 45 researchers, with interests and expertise in many different aspects of modelling and reasoning about mutable state, met to present their current work and discuss ongoing projects and open problems.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/DagSemProc.04381.1
04381 Abstracts Collection – Dependently Typed Programming

Authors: Thorsten Altenkirch, Martin Hofmann, and John Hughes

Published in: Dagstuhl Seminar Proceedings, Volume 4381, Dependently Typed Programming (2005)

Abstract
From 12.09.04 to 17.09.04, the Dagstuhl Seminar 04381 ``Dependently Typed Programming'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Thorsten Altenkirch, Martin Hofmann, and John Hughes. 04381 Abstracts Collection – Dependently Typed Programming. In Dependently Typed Programming. Dagstuhl Seminar Proceedings, Volume 4381, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:DagSemProc.04381.1,
  author =	{Altenkirch, Thorsten and Hofmann, Martin and Hughes, John},
  title =	{{04381 Abstracts Collection – Dependently Typed Programming}},
  booktitle =	{Dependently Typed Programming},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4381},
  editor =	{Thorsten Altenkirch and Martin Hofmann and John Hughes},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04381.1},
  URN =		{urn:nbn:de:0030-drops-1864},
  doi =		{10.4230/DagSemProc.04381.1},
  annote =	{Keywords: dependently typed programming}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact