Zobrazeno 1 - 10
of 65
pro vyhledávání: '"type inhabitation"'
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
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.
Publikováno v:
Proceedings of the ACM on Programming Languages. 1:1-26
This paper presents a new technique for automatically synthesizing SQL queries from natural language (NL). At the core of our technique is a new NL-based program synthesis methodology that combines semantic parsing techniques from the NLP community w
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::dc6102606dcfd04cfdb323a28399075c
https://doi.org/10.1145/3133887
https://doi.org/10.1145/3133887
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
Autor:
Gabriel Scherer
Publikováno v:
POPL 2017
POPL 2017, Jan 2017, Paris, France
POPL
POPL 2017, Jan 2017, Paris, France
POPL
The logical technique of focusing can be applied to the λ-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with βη-normal forms. Introducing a saturation
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4ab48c56253b49600920c8f28a80c77e
https://inria.hal.science/hal-01646064/file/finite-sums.pdf
https://inria.hal.science/hal-01646064/file/finite-sums.pdf
Autor:
Andrej Dudenhefner, Jakob Rehof
Publikováno v:
POPL
A notion of dimension in intersection typed λ-calculi is presented. The dimension of a typed λ-term is given by the minimal norm of an elaboration (a proof theoretic decoration) necessary for typing the term at its type, and, intuitively, measures
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b992a38b2ca7971bb9dd4e3248e3f284
https://doi.org/10.1145/3009837.3009862
https://doi.org/10.1145/3009837.3009862
Autor:
Alejandro Díaz-Caro, Pablo Arrighi
Publikováno v:
QPL 2009-International Workshop on Quantum Physics and Logic
QPL 2009-International Workshop on Quantum Physics and Logic, Apr 2009, Oxford, United Kingdom. pp.219-229, ⟨10.1016/j.entcs.2011.01.033⟩
QPL 2009-International Workshop on Quantum Physics and Logic, Apr 2009, Oxford, United Kingdom. pp.219-229, ⟨10.1016/j.entcs.2011.01.033⟩
The Linear-Algebraic @l-Calculus [Arrighi, P. and G. Dowek, Linear-algebraic @l-calculus: higher-order, encodings and confluence, Lecture Notes in Computer Science (RTA'08) 5117 (2008), pp. 17-31] extends the @l-calculus with the possibility of makin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cb094f1c20d60ec5ad2261510ba9162a
Publikováno v:
PLDI
Developing modern software 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 technique that synthe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::093bab0903dae3010d70fae762ccd23f
https://doi.org/10.1145/2491956.2462192
https://doi.org/10.1145/2491956.2462192
Publikováno v:
Annual Symposium on Principles of Programming Languages
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Jan 2004, pp.64-76, ⟨10.1145/964001.964007⟩
POPL
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Jan 2004, pp.64-76, ⟨10.1145/964001.964007⟩
POPL
International audience; We present a notion of η-long β-normal term for the typed lambda calculus with sums and prove, using Grothendieck logical relations, that every term is equivalent to one in normal form. Based on this development we give the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::062d5127491964b3f188f5b1c73e52c5
https://doi.org/10.1145/982962.964007
https://doi.org/10.1145/982962.964007