Name
Title | ||
|---|---|---|
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search. |
Abstract | ||
|---|---|---|
A new, comprehensive 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, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and the end products are simple, recursive decision procedures and counting functions. |
Year | Venue | DocType |
|---|---|---|
2016 | CoRR | Journal |
Volume | Citations | PageRank |
abs/1604.02086 | 0 | 0.34 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| José Espírito Santo | 1 | 62 | 10.79 |
| Ralph Matthes | 2 | 201 | 21.67 |
| Luis Pinto | 3 | 69 | 12.04 |