Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Floris van Doorn"'
Autor:
Jeremy Avigad, Floris van Doorn
Publikováno v:
2021 IEEE International Conference on Autonomous Systems (ICAS).
We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, $n$ drones surveil a finite interval, moving at uniform speed and exchanging informati
Autor:
Floris van Doorn, Jesse Michael Han
We describe a formal proof of the independence of the continuum hypothesis ($\mathsf{CH}$) in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for both directions, using Cohen forcing for the consistency of $\neg \maths
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::08bc0f9ed54d8b23eb98177afbfb0512
http://arxiv.org/abs/2102.02901
http://arxiv.org/abs/2102.02901
Publikováno v:
LICS
Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us
Publikováno v:
LICS
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c165fa322ffd100fce2f4c2ef8ca50d3
Publikováno v:
Interactive Theorem Proving ISBN: 9783319661063
ITP
ITP
We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7f2a3a054e5c697a98d6b62533797880
https://doi.org/10.1007/978-3-319-66107-0_30
https://doi.org/10.1007/978-3-319-66107-0_30
Autor:
Floris van Doorn
Publikováno v:
CPP
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characteriz
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0ca6e5266786cc6bb0e527ed18e83f1c
http://arxiv.org/abs/1512.02274
http://arxiv.org/abs/1512.02274
Publikováno v:
Automated Deduction-CADE-25 ISBN: 9783319214009
CADE
CADE
Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::53afc878adb74253a81a09a49d60cfb6
Autor:
Cody Roux, Floris van Doorn
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319089171
RTA-TLCA
RTA-TLCA
We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union \(\mathcal{P}+\mathc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::863631ca10e8c585e4c3e84227ea117c
https://doi.org/10.1007/978-3-319-08918-8_25
https://doi.org/10.1007/978-3-319-08918-8_25