3 Search Results for "Pitt, Jeremy"


Document
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis

Authors: Jesse Michael Han and Floris van Doorn

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model.

Cite as

Jesse Michael Han and Floris van Doorn. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{han_et_al:LIPIcs.ITP.2019.19,
  author =	{Han, Jesse Michael and van Doorn, Floris},
  title =	{{A Formalization of Forcing and the Unprovability of the Continuum Hypothesis}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.19},
  URN =		{urn:nbn:de:0030-drops-110742},
  doi =		{10.4230/LIPIcs.ITP.2019.19},
  annote =	{Keywords: Interactive theorem proving, formal verification, set theory, forcing, independence proofs, continuum hypothesis, Boolean-valued models, Lean}
}
Document
Social Concepts in Self-organising Systems (Dagstuhl Seminar 15482)

Authors: Ada Diaconescu, Stepehn Marsh, Jeremy Pitt, Wolfgang Reif, and Jan-Philipp Steghöfer

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15482 "Social Concepts in Self-organising Systems". The seminar brought together researchers from computer sciences (in particular from the fields of multi-agent systems and self-organisation) and from social sciences to discuss the impact of the use of social concepts in technical systems as well as the interaction between technical and social systems. In an engaging and interactive setting, the problem was illuminated from a technical as well as a philosophical and legal point of view. The talks, discussions, and working groups identified a growing body of work in the field, a number of interesting and promising research avenues, as well as a set of open issues for future investigation.

Cite as

Ada Diaconescu, Stepehn Marsh, Jeremy Pitt, Wolfgang Reif, and Jan-Philipp Steghöfer. Social Concepts in Self-organising Systems (Dagstuhl Seminar 15482). In Dagstuhl Reports, Volume 5, Issue 11, pp. 127-150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{diaconescu_et_al:DagRep.5.11.127,
  author =	{Diaconescu, Ada and Marsh, Stepehn and Pitt, Jeremy and Reif, Wolfgang and Stegh\"{o}fer, Jan-Philipp},
  title =	{{Social Concepts in Self-organising Systems (Dagstuhl Seminar 15482)}},
  pages =	{127--150},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{Diaconescu, Ada and Marsh, Stepehn and Pitt, Jeremy and Reif, Wolfgang and Stegh\"{o}fer, Jan-Philipp},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.11.127},
  URN =		{urn:nbn:de:0030-drops-57954},
  doi =		{10.4230/DagRep.5.11.127},
  annote =	{Keywords: computational justice, multi-agent sytems, norms, organic computing, reputation, self-organisation, social capital, socio-technical systems, sociologically-inspired computing, trust}
}
Document
Collective Adaptive Systems: Qualitative and Quantitative Modelling and Analysis (Dagstuhl Seminar 14512)

Authors: Jane Hillston, Jeremy Pitt, Martin Wirsing, and Franco Zambonelli

Published in: Dagstuhl Reports, Volume 4, Issue 12 (2015)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14512 "Collective Adaptive Systems: Qualitative and Quantitative Modelling and Analysis". Besides presentations on current work in the area, the seminar focused on the following topics: (i) Modelling techniques and languages for collective adaptive systems based on the above formalisms. (ii) Verification of collective adaptive systems. (iii) Humans-in-the-loop in collective adaptive systems.

Cite as

Jane Hillston, Jeremy Pitt, Martin Wirsing, and Franco Zambonelli. Collective Adaptive Systems: Qualitative and Quantitative Modelling and Analysis (Dagstuhl Seminar 14512). In Dagstuhl Reports, Volume 4, Issue 12, pp. 68-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{hillston_et_al:DagRep.4.12.68,
  author =	{Hillston, Jane and Pitt, Jeremy and Wirsing, Martin and Zambonelli, Franco},
  title =	{{Collective Adaptive Systems: Qualitative and Quantitative Modelling and Analysis (Dagstuhl Seminar 14512)}},
  pages =	{68--113},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{12},
  editor =	{Hillston, Jane and Pitt, Jeremy and Wirsing, Martin and Zambonelli, Franco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.12.68},
  URN =		{urn:nbn:de:0030-drops-50066},
  doi =		{10.4230/DagRep.4.12.68},
  annote =	{Keywords: Collective Adaptive Systems, Qualitative and Quantitative Modelling and Analysis, Verification, Humans-In-The-Loop}
}
  • Refine by Author
  • 2 Pitt, Jeremy
  • 1 Diaconescu, Ada
  • 1 Han, Jesse Michael
  • 1 Hillston, Jane
  • 1 Marsh, Stepehn
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Boolean-valued models
  • 1 Collective Adaptive Systems
  • 1 Humans-In-The-Loop
  • 1 Interactive theorem proving
  • 1 Lean
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2015
  • 1 2016
  • 1 2019

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