Zobrazeno 1 - 3
of 3
pro vyhledávání: '"Loïc Pujet"'
Autor:
Loïc Pujet, Nicolas Tabareau
Publikováno v:
POPL 2023 Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. pp.74, ⟨10.1145/3571739⟩
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. pp.74, ⟨10.1145/3571739⟩
International audience; In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredica
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::47771d66871d869f03c33deb8b658c38
https://doi.org/10.1145/3571739
https://doi.org/10.1145/3571739
Autor:
Loïc Pujet, Nicolas Tabareau
Publikováno v:
POPL
POPL, Jan 2022, Philadelphie, United States
Proceedings of the ACM on Programming Languages
POPL 2022: Symposium on Principles of Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2022, 6 (POPL), ⟨10.1145/3498693⟩
Proceedings of the ACM on Programming Languages, 2022, 6 (POPL), pp.1-29. ⟨10.1145/3498693⟩
POPL, Jan 2022, Philadelphie, United States
Proceedings of the ACM on Programming Languages
POPL 2022: Symposium on Principles of Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2022, 6 (POPL), ⟨10.1145/3498693⟩
Proceedings of the ACM on Programming Languages, 2022, 6 (POPL), pp.1-29. ⟨10.1145/3498693⟩
International audience; Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TT obs , a new type theory based on the setoidal interpretation of dependent type theory. TT obs
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5ee1676bbc23f2c9ee06579dabf1bc5e
https://hal.inria.fr/hal-03367052v3/document
https://hal.inria.fr/hal-03367052v3/document
Autor:
Anders Mörtberg, Loïc Pujet
Publikováno v:
CPP 2020-9th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2020-9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, New Orleans, United States. pp.1-14, ⟨10.1145/3372885.3373825⟩
CPP
CPP 2020-9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, New Orleans, United States. pp.1-14, ⟨10.1145/3372885.3373825⟩
CPP
International audience; Homotopy type theory is an extension of type theory that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations of multiple classical results from homotopy theory. However
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d1dd6c3bd38c3425dd418a599625ab5c
https://hal.archives-ouvertes.fr/hal-02394145/file/main.pdf
https://hal.archives-ouvertes.fr/hal-02394145/file/main.pdf