Name
Abstract | ||
|---|---|---|
The logical foundation of arithmetic generally starts with aquantificational logic over relations. Of course, one often wishes to have a formal treatment of functions within this setting. BothHilbert and Church added choice operators (such as the epsilonoperator) to logic in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that does not extend the underlying logic with either choice principles or with an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions. |
Year | Venue | Field |
|---|---|---|
2017 | CSL | ENCODE,Discrete mathematics,Algebra,Computer science,A-normal form,Mathematical proof,Operator (computer programming),Rewriting,Computation |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ulysse Gérard | 1 | 0 | 0.34 |
| Dale Miller | 2 | 2485 | 232.26 |