A parametricity-based formalization of semi-simplicial and semi-cubical sets

Autor: Herbelin, Hugo, Ramachandra, Ramkumar

Constructions such as semi-simplicial and semi-cubical sets can be defined in the "usual way" as presheaves over respectively, the semi-simplex or semi-cube category, which we call fibered definitions, but also defined like in e.g. Voevodsky or in pr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::158a3c9e0c8eae9fbc74eba0e7af30a7
https://inria.hal.science/hal-03963929/file/paper.pdf

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines

Autor: Dominique Larchey-Wendling, Yannick Forster

Publikováno v: CPP 2019 Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Jan 2019, Cascais, Portugal. pp.104-117, ⟨10.1145/3293880.3294096⟩
CPP

International audience; We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reduct

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::329a7bc40eaa85ae924df21c89ce90d8
https://hal.archives-ouvertes.fr/hal-02333390/document

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Theorem of three circles in Coq

Autor: Julianna Zsido

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, 2013, ⟨10.1007/s10817-013-9299-0⟩
Journal of Automated Reasoning, Springer Verlag, 2013, ⟨10.1007/s10817-013-9299-0⟩

The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong to a certa

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::64cf52220420472cdee88c9d44a73636
https://hal.inria.fr/hal-00864827

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.