Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/62948
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Matthes, Ralph | por |
dc.contributor.author | Pinto, Luís F. | por |
dc.date.accessioned | 2020-01-06T22:10:42Z | - |
dc.date.available | 2020-07-01T06:00:12Z | - |
dc.date.issued | 2019 | - |
dc.identifier.issn | 0960-1295 | por |
dc.identifier.uri | https://hdl.handle.net/1822/62948 | - |
dc.description.abstract | A new approach to inhabitation problems in simply typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda terms. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and produces simple, recursive decision procedures and counting functions. These allow to predict the number of inhabitants by testing the given type for syntactic criteria. This new approach is comprehensive and robust: based on the same syntactic representation, we also derive the state-of-the-art coherence theorems ensuring uniqueness of inhabitants. | por |
dc.description.sponsorship | We would like to thank our anonymous referees for their detailed and thoughtful reviews. The first and the last author were partially financed by Fundacao para a Ciencia e a Tecnologia (FCT) through project UID/MAT/00013/2013. The second author was partially financed by the project Climt, ANR-11-BS02-016, of the French Agence Nationale de la Recherche. All authors got financial support by the COST action CA15123 EUTYPES. | por |
dc.language.iso | eng | por |
dc.publisher | Cambridge University Press | por |
dc.relation | info:eu-repo/grantAgreement/FCT/5876/147370/PT | por |
dc.rights | openAccess | por |
dc.title | Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search | por |
dc.type | article | - |
dc.peerreviewed | yes | por |
oaire.citationStartPage | 1092 | por |
oaire.citationEndPage | 1124 | por |
oaire.citationIssue | 8 | por |
oaire.citationVolume | 29 | por |
dc.date.updated | 2020-01-04T21:04:52Z | - |
dc.identifier.eissn | 1469-8072 | por |
dc.identifier.doi | 10.1017/S0960129518000099 | por |
rcaap.embargofct | Política de arquivo da revista | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
dc.subject.wos | Science & Technology | - |
sdum.export.identifier | 5466 | - |
sdum.journal | Mathematical Structures in Computer Science | por |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
InhabitationThroughALambdaCalculusForProofSearch_Accepted.pdf | 425,48 kB | Adobe PDF | Ver/Abrir |