Zobrazeno 1 - 10
of 247
pro vyhledávání: '"Type inhabitation"'
Autor:
Dudenhefner, Andrej1 (AUTHOR) andrej.dudenhefner@cs.tu-dortmund.de, Rehof, Jakob1 (AUTHOR), Altenkirch, Thorsten (AUTHOR), Schubert, Aleksy (AUTHOR)
Publikováno v:
Fundamenta Informaticae. 2019, Vol. 170 Issue 1-3, p93-110. 18p.
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
M Clarence Protin
Publikováno v:
Journal of Logic and Computation. 31:416-425
Atomic polymorphism $\mathbf{F_{at}}$ is a restriction of Girard and Reynold’s system $\mathbf{F} $(or $\lambda 2$) which was first introduced in Ferreira [ 2] in the context of a philosophical commentary on predicativism. $\lambda 2$ is a well-kno
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::fc0e85235a6ace8f79cd6af1fb4e6b69
https://doi.org/10.1093/logcom/exaa090
https://doi.org/10.1093/logcom/exaa090
Autor:
Andrej Dudenhefner, Jakob Rehof
Publikováno v:
Fundamenta Informaticae. 170:93-110
We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we simplify the existing proof, reducing simple semi-Thue systems to intersection type inhabitation in the original Coppo-De
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7720b984744486b9f531eb909babb20e
https://doi.org/10.3233/fi-2019-1856
https://doi.org/10.3233/fi-2019-1856
Autor:
Łukasz Czajka
Publikováno v:
Automated Reasoning ISBN: 9783030510534
We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as large
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::708fa4e8d597cab10723afd242a753ea
https://doi.org/10.1007/978-3-030-51054-1_3
https://doi.org/10.1007/978-3-030-51054-1_3
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Czajka, Łukasz
Publikováno v:
Automated Reasoning
We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as large
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pmc_________::01cde66d25ed31327f3b3e5bc7481068
http://europepmc.org/articles/PMC7324019
http://europepmc.org/articles/PMC7324019
Autor:
Sandra Alves, Sabine Broda
Publikováno v:
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
A correspondence between the formula-tree of a type and the arena associated to a type.A correspondence between proof-trees and winning strategies in a game.A proof of the equivalence between the formula-tree method and the method based on game seman
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6117546618837bd980c0265a1d352778
http://repositorio.inesctec.pt/handle/123456789/5222
http://repositorio.inesctec.pt/handle/123456789/5222
Conference
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a techniqu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______185::71407b9bb5aebd64de9877ea8d7b21a1
https://infoscience.epfl.ch/record/170040
https://infoscience.epfl.ch/record/170040