Home > Research > Publications & Outputs > Reasoning about Dynamic Auctions

Research

Links

View graph of relations

Reasoning about Dynamic Auctions

Research output: Contribution to conference - Without ISBN/ISSN › Conference paper › peer-review

Published

Standard

Reasoning about Dynamic Auctions. / Caminati, Marco; Kerber, Manfred; Rowat, Colin.
2015.

Research output: Contribution to conference - Without ISBN/ISSN › Conference paper › peer-review

Harvard

Caminati, M, Kerber, M & Rowat, C 2015, 'Reasoning about Dynamic Auctions'. <https://dokumen.tips/documents/proceedings-of-the-automated-reasoning-workshop-2015-bridging-2017-12-16-proceedings.html?page=1>

APA

Caminati, M., Kerber, M., & Rowat, C. (2015). Reasoning about Dynamic Auctions. https://dokumen.tips/documents/proceedings-of-the-automated-reasoning-workshop-2015-bridging-2017-12-16-proceedings.html?page=1

Vancouver

Caminati M, Kerber M, Rowat C. Reasoning about Dynamic Auctions. 2015.

Author

Caminati, Marco ; Kerber, Manfred ; Rowat, Colin. / Reasoning about Dynamic Auctions.

Bibtex

@conference{205ff865c6b14b6781da4fee3350140e,
title = "Reasoning about Dynamic Auctions",
abstract = "Auctions are used to sell goods worth trillions of dollars annually.Many of them are well established, frequently used, and hence well tested.However, in some domains new auction schemes are developed and only infrequently used. These can benefit most from formal methods.We report here how verified code can be extracted using Isabelle's extraction mechanism for so-called dynamic auctions, that is, auctions in which participants can bid in several rounds.We use co-recursion in order to reason about and extract code for dynamic auctions in which inputs and computations are interleaved.",
author = "Marco Caminati and Manfred Kerber and Colin Rowat",
year = "2015",
month = apr,
day = "30",
language = "English",

}

RIS

TY - CONF

T1 - Reasoning about Dynamic Auctions

AU - Caminati, Marco

AU - Kerber, Manfred

AU - Rowat, Colin

PY - 2015/4/30

Y1 - 2015/4/30

N2 - Auctions are used to sell goods worth trillions of dollars annually.Many of them are well established, frequently used, and hence well tested.However, in some domains new auction schemes are developed and only infrequently used. These can benefit most from formal methods.We report here how verified code can be extracted using Isabelle's extraction mechanism for so-called dynamic auctions, that is, auctions in which participants can bid in several rounds.We use co-recursion in order to reason about and extract code for dynamic auctions in which inputs and computations are interleaved.

AB - Auctions are used to sell goods worth trillions of dollars annually.Many of them are well established, frequently used, and hence well tested.However, in some domains new auction schemes are developed and only infrequently used. These can benefit most from formal methods.We report here how verified code can be extracted using Isabelle's extraction mechanism for so-called dynamic auctions, that is, auctions in which participants can bid in several rounds.We use co-recursion in order to reason about and extract code for dynamic auctions in which inputs and computations are interleaved.

M3 - Conference paper

ER -