λ
In: Automated deduction - CADE-19 (Miami Beach FL, 28 July - 2 August 2003)Lecture notes in computer science :136-150
Konferenz
- print, 26 ref
Zugriff:
We make the notion of scope in the A-calculus explicit. To that end, the syntax of the A-calculus is extended with an end-of-scope operator A, matching the usual opening of a scope due to A. Accordingly, β-reduction is extended to the set of scoped A-terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped β-reduction. Confluence of β-reduction for the ordinary A-calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, α-equivalence is needed. All our proofs have been verified in Coq.
Titel: |
λ
|
---|---|
Autor/in / Beteiligte Person: | HENDRIKS, Dimitri ; VAN OOSTROM, Vincent |
Link: | |
Quelle: | Automated deduction - CADE-19 (Miami Beach FL, 28 July - 2 August 2003)Lecture notes in computer science :136-150 |
Veröffentlichung: | Berlin: Springer, 2003 |
Medientyp: | Konferenz |
Umfang: | print, 26 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|