Name
Abstract | ||
|---|---|---|
Filter models and (solutions of) recursive domain equations are two different ways of constructing lambda models. Many partial results have been shown about the equivalence between these two constructions (in some specific cases). This paper deepens the connection by showing that the equivalence can be shown in a general framework. We will introduce the class of disciplined intersection type theories and its four subclasses: natural split, lazy split, natural equated and lazy equated. We will prove that each class corresponds to a different recursive domain equation. For this result, we are extracting the essence of the specific proofs for the particular cases of intersection type theories and making one general construction that encompasses all of them. This general approach puts together all these results which may appear scattered and sometimes with incomplete proofs in the literature. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-77566-9_11 | SOFSEM |
Keywords | Field | DocType |
lazy split,different way,different recursive domain equation,general construction,natural split,intersection type theory,general framework,class corresponds,recursive domain equation,general approach,disciplined intersection type theory,filter model | Galois connection,Discrete mathematics,Combinatorics,Type theory,Equivalence (measure theory),Mathematical proof,Complete lattice,Recursion,Mathematics,Lambda | Conference |
Volume | ISSN | ISBN |
4910 | 0302-9743 | 3-540-77565-X |
Citations | PageRank | References |
1 | 0.38 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Fabio Alessi | 1 | 83 | 12.04 |
| Paula Severi | 2 | 122 | 16.19 |