7 Search Results for "Krivine, Jean-Louis"

Document
DOI: 10.4230/LIPIcs.CSL.2024.28
Realizability Models for Large Cardinals

Authors: Laura Fontanella, Guillaume Geoffroy, and Richard Matthews

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Realizabilty is a branch of logic that aims at extracting the computational content of mathematical proofs by establishing a correspondence between proofs and programs. Invented by S.C. Kleene in the 1945 to develop a connection between intuitionism and Turing computable functions, realizability has evolved to include not only classical logic but even set theory, thanks to the work of J-L. Krivine. Krivine’s work made possible to build realizability models for Zermelo-Frænkel set theory, ZF, assuming its consistency. Nevertheless, a large part of set theoretic research involves investigating further axioms that are known as large cardinals axioms; in this paper we focus on four large cardinals axioms: the axioms of (strongly) inaccessible cardinal, Mahlo cardinals, measurable cardinals and Reinhardt cardinals. We show how to build realizability models for each of these four axioms assuming their consistency relative to ZFC or ZF.
Cite as

Laura Fontanella, Guillaume Geoffroy, and Richard Matthews. Realizability Models for Large Cardinals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fontanella_et_al:LIPIcs.CSL.2024.28,
  author =	{Fontanella, Laura and Geoffroy, Guillaume and Matthews, Richard},
  title =	{{Realizability Models for Large Cardinals}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.28},
  URN =		{urn:nbn:de:0030-drops-196715},
  doi =		{10.4230/LIPIcs.CSL.2024.28},
  annote =	{Keywords: Logic, Classical Realizability, Set Theory, Large Cardinals}
}
Document
Short Paper
DOI: 10.4230/OASIcs.Tokenomics.2020.10
Revisiting the Liquidity/Risk Trade-Off with Smart Contracts (Short Paper)

Authors: Vincent Danos, Jean Krivine, and Julien Prat

Published in: OASIcs, Volume 82, 2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)

Abstract
Real-time financial settlements constrain traders to have the cash on hand before they can enter a trade [Khapko and Zoican, 2017]. This prevents short-selling and ultimately impedes liquidity. We propose a novel trading protocol which relaxes the cash constraint, and manages chains of deferred payments. Traders can buy without paying first, and can re-sell while still withholding payments. Trades naturally arrange in chains which contract when deals are closed and extend when new ones open. Default risk is handled by reversing trades. In this short note we propose a class of novel financial instruments for zero-risk and zero-collateral intermediation. The central idea is that bilateral trades can be chained into trade lines. The ownership of an underlying asset becomes distributed among traders with positions in the trade line. The trading protocol determines who ends up owning that asset and the overall payoffs of the participants. Counterparty risk is avoided because the asset itself serves as a collateral for the entire chain of trades. The protocol can be readily implemented as a smart contract on a blockchain. Additional examples, proofs, protocol variants, and game-theoretic properties related to the order-sensitivity of the games defined by trade lines can be found in the extended version of this note [Danos et al., 2019]. Therein, one can also find the definition and game-theoretic analysis of standard trade-lines with applications to trust-less zero-collateral intermediation.
Cite as

Vincent Danos, Jean Krivine, and Julien Prat. Revisiting the Liquidity/Risk Trade-Off with Smart Contracts (Short Paper). In 2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020). Open Access Series in Informatics (OASIcs), Volume 82, pp. 10:1-10:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{danos_et_al:OASIcs.Tokenomics.2020.10,
  author =	{Danos, Vincent and Krivine, Jean and Prat, Julien},
  title =	{{Revisiting the Liquidity/Risk Trade-Off with Smart Contracts}},
  booktitle =	{2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)},
  pages =	{10:1--10:5},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-157-3},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{82},
  editor =	{Anceaume, Emmanuelle and Bisi\`{e}re, Christophe and Bouvard, Matthieu and Bramas, Quentin and Casamatta, Catherine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Tokenomics.2020.10},
  URN =		{urn:nbn:de:0030-drops-135325},
  doi =		{10.4230/OASIcs.Tokenomics.2020.10},
  annote =	{Keywords: Electronic trading, Smart contracts, Static analysis}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.9
Causal Unfoldings

Authors: Marc de Visme and Glynn Winskel

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
In the simplest form of event structure, a prime event structure, an event is associated with a unique causal history, its prime cause. However, it is quite common for an event to have disjunctive causes in that it can be enabled by any one of multiple sets of causes. Sometimes the sets of causes may be mutually exclusive, inconsistent one with another, and sometimes not, in which case they coexist consistently and constitute parallel causes of the event. The established model of general event structures can model parallel causes. On occasion however such a model abstracts too far away from the precise causal histories of events to be directly useful. For example, sometimes one needs to associate probabilities with different, possibly coexisting, causal histories of a common event. Ideally, the causal histories of a general event structure would correspond to the configurations of its causal unfolding to a prime event structure; and the causal unfolding would arise as a right adjoint to the embedding of prime in general event structures. But there is no such adjunction. However, a slight extension of prime event structures remedies this defect and provides a causal unfolding as a universal construction. Prime event structures are extended with an equivalence relation in order to dissociate the two roles, that of an event and its enabling; in effect, prime causes are labelled by a disjunctive event, an equivalence class of its prime causes. With this enrichment a suitable causal unfolding appears as a pseudo right adjoint. The adjunction relies critically on the central and subtle notion of extremal causal realisation as an embodiment of causal history.
Cite as

Marc de Visme and Glynn Winskel. Causal Unfoldings. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{devisme_et_al:LIPIcs.CALCO.2019.9,
  author =	{de Visme, Marc and Winskel, Glynn},
  title =	{{Causal Unfoldings}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.9},
  URN =		{urn:nbn:de:0030-drops-114376},
  doi =		{10.4230/LIPIcs.CALCO.2019.9},
  annote =	{Keywords: Event Structures, Parallel Causes, Causal Unfolding, Probability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.25
Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

Authors: Jean-Louis Krivine

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
This paper is about the bar recursion operator in the context of classical realizability. The pioneering work of Berardi, Bezem, Coquand was enhanced by Berger and Oliva. Then Streicher has shown, by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of lambda-calculus (Scott domains, coherent spaces, ...), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of R and the continuum hypothesis. These formulas are therefore realized by closed lambda_c-terms. This new result allows to obtain programs from proofs of arithmetical formulas using all these axioms.
Cite as

Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 25:1-25:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.CSL.2016.25,
  author =	{Krivine, Jean-Louis},
  title =	{{Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{25:1--25:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.25},
  URN =		{urn:nbn:de:0030-drops-65650},
  doi =		{10.4230/LIPIcs.CSL.2016.25},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.146
On the Structure of Classical Realizability Models of ZF

Authors: Jean-Louis Krivine

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
The technique of classical realizability is an extension of the method of forcing; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called realizability models. The structure of these models is, in general, much more complicated than that of the particular case of forcing models. We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical). By Shoenfield absoluteness theorem, it follows that every true Sigma^1_3 formula is realized by a closed lambda_c-term.
Cite as

Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 146-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.TYPES.2014.146,
  author =	{Krivine, Jean-Louis},
  title =	{{On the Structure of Classical Realizability Models of ZF}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{146--161},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146},
  URN =		{urn:nbn:de:0030-drops-54953},
  doi =		{10.4230/LIPIcs.TYPES.2014.146},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}
Document
DOI: 10.4230/DagRep.2.8.99
Information Flow and Its Applications (Dagstuhl Seminar 12352)

Authors: Samson Abramsky, Jean Krivine, and Michael W. Mislove

Published in: Dagstuhl Reports, Volume 2, Issue 8 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12352 "Information Flow and Its Applications". This seminar brought together mathematicians, computer scientists, physicists and researchers from related disciplines such as computational biology who are working on problems concerning information and information flow.
Cite as

Samson Abramsky, Jean Krivine, and Michael W. Mislove. Information Flow and Its Applications (Dagstuhl Seminar 12352). In Dagstuhl Reports, Volume 2, Issue 8, pp. 99-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{abramsky_et_al:DagRep.2.8.99,
  author =	{Abramsky, Samson and Krivine, Jean and Mislove, Michael W.},
  title =	{{Information Flow and Its Applications (Dagstuhl Seminar 12352)}},
  pages =	{99--112},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{8},
  editor =	{Abramsky, Samson and Krivine, Jean and Mislove, Michael W.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.8.99},
  URN =		{urn:nbn:de:0030-drops-37866},
  doi =		{10.4230/DagRep.2.8.99},
  annote =	{Keywords: Information flow; semantics of computation; quantum computing; systems biology; information theory; informatics}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.276
Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models

Authors: Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh, and Glynn Winskel

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

Abstract
In this paper, we introduce a novel way of constructing concise causal histories (pathways) to represent how specified structures are formed during simulation of systems represented by rule-based models. This is founded on a new, clean, graph-based semantics introduced in the first part of this paper for Kappa, a rule-based modelling language that has emerged as a natural description of protein-protein interactions in molecular biology [Bachman 2011]. The semantics is capable of capturing the whole of Kappa, including subtle side-effects on deletion of structure, and its structured presentation provides the basis for the translation of techniques to other models. In particular, we give a notion of trajectory compression, which restricts a trace culminating in the production of a given structure to the actions necessary for the structure to occur. This is central to the reconstruction of biochemical pathways due to the failure of traditional techniques to provide adequately concise causal histories, and we expect it to be applicable in a range of other modelling situations.
Cite as

Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh, and Glynn Winskel. Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 276-288, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{danos_et_al:LIPIcs.FSTTCS.2012.276,
  author =	{Danos, Vincent and Feret, Jerome and Fontana, Walter and Harmer, Russell and Hayman, Jonathan and Krivine, Jean and Thompson-Walsh, Chris and Winskel, Glynn},
  title =	{{Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{276--288},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.276},
  URN =		{urn:nbn:de:0030-drops-38669},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.276},
  annote =	{Keywords: concurrency, rule-based models, graph rewriting, pathways, causality}
}
  • Refine by Author
  • 3 Krivine, Jean
  • 2 Danos, Vincent
  • 2 Krivine, Jean-Louis
  • 2 Winskel, Glynn
  • 1 Abramsky, Samson
  • Show More...

  • Refine by Classification
  • 1 Information systems → Online banking
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Curry-Howard correspondence
  • 2 lambda-calculus
  • 2 set theory
  • 1 Causal Unfolding
  • 1 Classical Realizability
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 1 2012
  • 1 2013
  • 1 2015
  • 1 2016
  • 1 2019
  • Show More...

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