Zobrazeno 1 - 5
of 5
pro vyhledávání: '"Kuen-Bang Hou (Favonia)"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 1-10 (2018)
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish b
Externí odkaz:
https://doaj.org/article/86dcd954605c4cb2ac77f3daa3801932
Autor:
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Publikováno v:
Mathematical Structures in Computer Science. 31:424-468
We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5ed2b2c96ba07fa76e844ad793228f2e
https://doi.org/10.1017/s0960129521000347
https://doi.org/10.1017/s0960129521000347
Autor:
Ulrik Buchholtz, Kuen-Bang Hou Favonia
Publikováno v:
LICS
Logical Methods in Computer Science ; Volume 16, Issue 2 ; 1860-5974
We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and h
We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and h
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::41049a52e3429b799b77f960c42702d8
http://arxiv.org/abs/1802.02191
http://arxiv.org/abs/1802.02191
Autor:
Kuen-Bang Hou (Favonia)
Mechanized reasoning has proved effective in avoiding serious mistakes in software and hardware, and yet remains unpopular in the practice of mathematics. My thesis is aimed at making mechanization easier so that more mathematicians can benefit from
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9bb81d90d75e1dfdb8d443e7de16f39d
Publikováno v:
LICS
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a resul
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ed6e851a5b2c045304a28072020b0328
https://doi.org/10.1145/2933575.2934545
https://doi.org/10.1145/2933575.2934545