Search Results

Documents authored by Jones, Michael Peyton

Found 2 Possible Name Variants:

Jones, Michael A.

Document
DOI: 10.4230/DagSemProc.07261.5
Better Ways to Cut a Cake - Revisited

Authors: Steven J. Brams, Michael A. Jones, and Christian Klamler

Published in: Dagstuhl Seminar Proceedings, Volume 7261, Fair Division (2007)

Abstract
Procedures to divide a cake among n people with n-1 cuts (the minimum number) are analyzed and compared. For 2 persons, cut-and-choose, while envy-free and efficient, limits the cutter to exactly 50% if he or she is ignorant of the chooser's preferences, whereas the chooser can generally obtain more. By comparison, a new 2-person surplus procedure (SP'), which induces the players to be truthful in order to maximize their minimum allocations, leads to a proportionally equitable division of the surplus - the part that remains after each player receives 50% - by giving each person a certain proportion of the surplus as he or she values it. For n geq 3 persons, a new equitable procedure (EP) yields a maximally equitable division of a cake. This division gives all players the highest common value that they can achieve and induces truthfulness, but it may not be envy-free. The applicability of SP' and EP to the fair division of a heterogeneous, divisible good, like land, is briefly discussed.
Cite as

Steven J. Brams, Michael A. Jones, and Christian Klamler. Better Ways to Cut a Cake - Revisited. In Fair Division. Dagstuhl Seminar Proceedings, Volume 7261, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{brams_et_al:DagSemProc.07261.5,
  author =	{Brams, Steven J. and Jones, Michael A. and Klamler, Christian},
  title =	{{Better Ways to Cut a Cake - Revisited}},
  booktitle =	{Fair Division},
  pages =	{1--24},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7261},
  editor =	{Steven Brams and Kirk Pruhs and Gerhard Woeginger},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07261.5},
  URN =		{urn:nbn:de:0030-drops-12278},
  doi =		{10.4230/DagSemProc.07261.5},
  annote =	{Keywords: Fair division, cake-cutting, envy-freeness, strategy-proofness}
}
Document
DOI: 10.4230/DagSemProc.07261.6
Divide-and-Conquer: A Proportional, Minimal-Envy Cake-Cutting Procedure

Authors: Steven J. Brams, Michael A. Jones, and Christian Klamler

Published in: Dagstuhl Seminar Proceedings, Volume 7261, Fair Division (2007)

Abstract
Properties of discrete cake-cutting procedures that use a minimal number of cuts (n-1 if there are n players) are analyzed. None is always envy-free or efficient, but divide-and-conquer (D&C) minimizes the maximum number of players that any single player may envy. It works by asking n ≥ 2 players successively to place marks on a cake that divide it into equal or approximately equal halves, then halves of these halves, and so on. Among other properties, D&C (i) ensures players of more than 1/n shares if their marks are different and (ii) is strategyproof for risk-averse players. However, D&C may not allow players to obtain proportional, connected pieces if they have unequal entitlements. Possible applications of D&C to land division are briefly discussed.
Cite as

Steven J. Brams, Michael A. Jones, and Christian Klamler. Divide-and-Conquer: A Proportional, Minimal-Envy Cake-Cutting Procedure. In Fair Division. Dagstuhl Seminar Proceedings, Volume 7261, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{brams_et_al:DagSemProc.07261.6,
  author =	{Brams, Steven J. and Jones, Michael A. and Klamler, Christian},
  title =	{{Divide-and-Conquer: A Proportional, Minimal-Envy Cake-Cutting Procedure}},
  booktitle =	{Fair Division},
  pages =	{1--31},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7261},
  editor =	{Steven Brams and Kirk Pruhs and Gerhard Woeginger},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07261.6},
  URN =		{urn:nbn:de:0030-drops-12211},
  doi =		{10.4230/DagSemProc.07261.6},
  annote =	{Keywords: Cake-cutting, proportionality, envy-freeness, efficiency, strategy-proofness}
}
Document
DOI: 10.4230/DagSemProc.07261.11
Some Recent Results on Pie Cutting

Authors: Michael A. Jones

Published in: Dagstuhl Seminar Proceedings, Volume 7261, Fair Division (2007)

Abstract
For cake cutting, cuts are parallel to an axis and yield rectangular pieces. As such, cutting a cake is viewed as dividing a line segment. For pie cutting, cuts are radial from the center of a disc to the circumference and yield sectors or wedge-shaped pieces. As such, cutting a pie is viewed as dividing a circle. There is clearly a relationship between cutting a cake and cutting a pie. Once a circular pie has a single cut, then it can be straightened out into a segment, looking like a cake. Isn't a cake just a pie that has been cut? Gale (1993) suggested that this topology was a significant difference. This note is to summarize and compare some of the recent results on pie cutting that appear in Barbanel and Brams (2007) and Brams, Jones, and Klamler (2007). The geometric framework presented in Barbanel and Brams (2007) is used to prove and to explain results in Brams, Jones, and Klamler (2007).
Cite as

Michael A. Jones. Some Recent Results on Pie Cutting. In Fair Division. Dagstuhl Seminar Proceedings, Volume 7261, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{jones:DagSemProc.07261.11,
  author =	{Jones, Michael A.},
  title =	{{Some Recent Results on Pie Cutting}},
  booktitle =	{Fair Division},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7261},
  editor =	{Steven Brams and Kirk Pruhs and Gerhard Woeginger},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07261.11},
  URN =		{urn:nbn:de:0030-drops-12246},
  doi =		{10.4230/DagSemProc.07261.11},
  annote =	{Keywords: Pie cutting, envy-free, proportional, undominated}
}

Jones, Michael Peyton

Document
DOI: 10.4230/OASIcs.FMBC.2024.10
Structured Contracts in the EUTxO Ledger Model

Authors: Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain ledgers based on the extended UTxO model support fully expressive smart contracts to specify permissions for performing certain actions, such as spending transaction outputs or minting assets. There have been some attempts to standardize the implementation of stateful programs using this infrastructure, with varying degrees of success. To remedy this, we introduce the framework of structured contracts to formalize what it means for a stateful program to be correctly implemented on the ledger. Using small-step semantics, our approach relates low-level ledger transitions to high-level transitions of the smart contract being specified, thus allowing users to prove that their abstract specification is adequately realized on the blockchain. We argue that the framework is versatile enough to cover a range of examples, in particular proving the equivalence of multiple concrete implementations of the same abstract specification. Building upon prior meta-theoretical results, our results have been mechanized in the Agda proof assistant, paving the way to rigorous verification of smart contracts.
Cite as

Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu. Structured Contracts in the EUTxO Ledger Model. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vinogradova_et_al:OASIcs.FMBC.2024.10,
  author =	{Vinogradova, Polina and Melkonian, Orestis and Wadler, Philip and Chakravarty, Manuel and Krijnen, Jacco and Jones, Michael Peyton and Chapman, James and Ferariu, Tudor},
  title =	{{Structured Contracts in the EUTxO Ledger Model}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{10:1--10:19},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.10},
  URN =		{urn:nbn:de:0030-drops-198757},
  doi =		{10.4230/OASIcs.FMBC.2024.10},
  annote =	{Keywords: blockchain, ledger, smart contract, formal verification, specification, transition systems, Agda, UTxO, EUTxO, small-step semantics}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.2
QL: Object-oriented Queries on Relational Data

Authors: Pavel Avgustinov, Oege de Moor, Michael Peyton Jones, and Max Schäfer

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
This paper describes QL, a language for querying complex, potentially recursive data structures. QL compiles to Datalog and runs on a standard relational database, yet it provides familiar-looking object-oriented features such as classes and methods, reinterpreted in logical terms: classes are logical properties describing sets of values, subclassing is implication, and virtual calls are dispatched dynamically by considering the most specific classes containing the receiver. Furthermore, types in QL are prescriptive and actively influence program evaluation rather than just describing it. In combination, these features enable the development of concise queries based on reusable libraries, which are written in a purely declarative style, yet can be efficiently executed even on very large data sets. In particular, we have used QL to implement static analyses for various programming languages, which scale to millions of lines of code.
Cite as

Pavel Avgustinov, Oege de Moor, Michael Peyton Jones, and Max Schäfer. QL: Object-oriented Queries on Relational Data. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 2:1-2:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{avgustinov_et_al:LIPIcs.ECOOP.2016.2,
  author =	{Avgustinov, Pavel and de Moor, Oege and Jones, Michael Peyton and Sch\"{a}fer, Max},
  title =	{{QL: Object-oriented Queries on Relational Data}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{2:1--2:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.2},
  URN =		{urn:nbn:de:0030-drops-60968},
  doi =		{10.4230/LIPIcs.ECOOP.2016.2},
  annote =	{Keywords: Object orientation, Datalog, query languages, prescriptive typing}
}
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 About DROPS Imprint Privacy Contact