5 Search Results for "Leyton-Brown, Kevin"

Document
DOI: 10.4230/LIPIcs.ITP.2023.23
A Formalisation of Gallagher’s Ergodic Theorem

Authors: Oliver Nash

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Gallagher’s ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking "all or nothing" behaviour. We discuss a formalisation of this result in the Lean theorem prover. As well as being notable in its own right, the result is a key preliminary, required for Koukoulopoulos and Maynard’s stunning recent proof of the Duffin-Schaeffer conjecture.
Cite as

Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nash:LIPIcs.ITP.2023.23,
  author =	{Nash, Oliver},
  title =	{{A Formalisation of Gallagher’s Ergodic Theorem}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.23},
  URN =		{urn:nbn:de:0030-drops-183981},
  doi =		{10.4230/LIPIcs.ITP.2023.23},
  annote =	{Keywords: Lean proof assistant, measure theory, metric number theory, ergodicity, Gallagher’s theorem, Duffin-Schaeffer conjecture}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.9
The Next 700 Semantics: A Research Challenge

Authors: Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
Modern systems consist of large numbers of languages, frameworks, libraries, APIs, and more. Each has characteristic behavior and data. Capturing these in semantics is valuable not only for understanding them but also essential for formal treatment (such as proofs). Unfortunately, most of these systems are defined primarily through implementations, which means the semantics needs to be learned. We describe the problem of learning a semantics, provide a structuring process that is of potential value, and also outline our failed attempts at achieving this so far.
Cite as

Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty. The Next 700 Semantics: A Research Challenge. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{krishnamurthi_et_al:LIPIcs.SNAPL.2019.9,
  author =	{Krishnamurthi, Shriram and Lerner, Benjamin S. and Elberty, Liam},
  title =	{{The Next 700 Semantics: A Research Challenge}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.9},
  URN =		{urn:nbn:de:0030-drops-105522},
  doi =		{10.4230/LIPIcs.SNAPL.2019.9},
  annote =	{Keywords: Programming languages, desugaring, semantics, testing}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.238
Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems

Authors: Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth, Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov, Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel, and Kunle Olukotun

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Most performance critical software is developed using very low-level techniques. We argue that this needs to change, and that generative programming is an effective avenue to enable the use of high-level languages and programming techniques in many such circumstances.
Cite as

Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth, Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov, Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel, and Kunle Olukotun. Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 238-261, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{rompf_et_al:LIPIcs.SNAPL.2015.238,
  author =	{Rompf, Tiark and Brown, Kevin J. and Lee, HyoukJoong and Sujeeth, Arvind K. and Jonnalagedda, Manohar and Amin, Nada and Ofenbeck, Georg and Stojanov, Alen and Klonatos, Yannis and Dashti, Mohammad and Koch, Christoph and P\"{u}schel, Markus and Olukotun, Kunle},
  title =	{{Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{238--261},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.238},
  URN =		{urn:nbn:de:0030-drops-50295},
  doi =		{10.4230/LIPIcs.SNAPL.2015.238},
  annote =	{Keywords: Performance, Generative Programming, Staging, DSLs}
}
Document
DOI: 10.4230/DagSemProc.05011.6
Computing Nash Equilibria of Action-Graph Games

Authors: Kevin Leyton-Brown and Navin A.R. Bhat

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)

Abstract
This talk will survey two graphical models which the authors have proposed for compactly representing single-shot, finite-action games in which a large number of agents contend for scarce resources. The first model considered is Local-Effect Games (LEGs). These games often (but not always) have pure-strategy Nash equilibria. Finding a potential function is a good technique for finding such equilibria. We give a complete characterization of which LEGs have potential functions and provide the functions in each case; we also show a general case where pure-strategy equilibria exist in the absence of potential functions. Action-graph games (AGGs) are a fully expressive game representation which can compactly express both strict and context-specific independence between players' utility functions, and which generalize LEGs. We present algorithms for computing both symmetric and arbitrary equilibria of AGGs, based on a continuation method proposed by Govindan and Wilson. We analyze the worst- case cost of computing the Jacobian of the payoff function, the exponential- time bottleneck step of this algorithm, and in all cases achieve exponential speedup. When the indegree of G is bounded by a constant and the game is symmetric, the Jacobian can be computed in polynomial time.
Cite as

Kevin Leyton-Brown and Navin A.R. Bhat. Computing Nash Equilibria of Action-Graph Games. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{leytonbrown_et_al:DagSemProc.05011.6,
  author =	{Leyton-Brown, Kevin and Bhat, Navin A.R.},
  title =	{{Computing Nash Equilibria of Action-Graph Games}},
  booktitle =	{Computing and Markets},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.6},
  URN =		{urn:nbn:de:0030-drops-2209},
  doi =		{10.4230/DagSemProc.05011.6},
  annote =	{Keywords: compact representation of games, action-graph games, Nash equilibria}
}
Document
DOI: 10.4230/DagSemProc.05011.11
Local-Effect Games

Authors: Kevin Leyton-Brown and Moshe Tennenholtz

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)

Abstract
This talk will survey two graphical models which the authors have proposed for compactly representing single-shot, finite-action games in which a large number of agents contend for scarce resources. The first model considered is Local-Effect Games (LEGs). These games often (but not always) have pure-strategy Nash equilibria. Finding a potential function is a good technique for finding such equilibria. We give a complete characterization of which LEGs have potential functions and provide the functions in each case; we also show a general case where pure-strategy equilibria exist in the absence of potential functions. Action-graph games (AGGs) are a fully expressive game representation which can compactly express both strict and context-specific independence between players' utility functions, and which generalize LEGs. We present algorithms for computing both symmetric and arbitrary equilibria of AGGs, based on a continuation method proposed by Govindan and Wilson. We analyze the worst- case cost of computing the Jacobian of the payoff function, the exponential- time bottleneck step of this algorithm, and in all cases achieve exponential speedup. When the indegree of G is bounded by a constant and the game is symmetric, the Jacobian can be computed in polynomial time.
Cite as

Kevin Leyton-Brown and Moshe Tennenholtz. Local-Effect Games. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{leytonbrown_et_al:DagSemProc.05011.11,
  author =	{Leyton-Brown, Kevin and Tennenholtz, Moshe},
  title =	{{Local-Effect Games}},
  booktitle =	{Computing and Markets},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.11},
  URN =		{urn:nbn:de:0030-drops-2190},
  doi =		{10.4230/DagSemProc.05011.11},
  annote =	{Keywords: compact representation of games, congestion games, local-effect}
}
  • Refine by Author
  • 2 Leyton-Brown, Kevin
  • 1 Amin, Nada
  • 1 Bhat, Navin A.R.
  • 1 Brown, Kevin J.
  • 1 Dashti, Mohammad
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Probability and statistics
  • 1 Software and its engineering → Formal language definitions
  • 1 Software and its engineering → General programming languages
  • 1 Software and its engineering → Language features
  • 1 Software and its engineering → Semantics

  • Refine by Keyword
  • 2 compact representation of games
  • 1 DSLs
  • 1 Duffin-Schaeffer conjecture
  • 1 Gallagher’s theorem
  • 1 Generative Programming
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2005
  • 1 2015
  • 1 2019
  • 1 2023

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