Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
| Autor: | Masayuki Mizuno, Eijiro Sumii |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Algebra
Evaluation strategy TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering 020207 software engineering 020201 artificial intelligence & image processing 02 engineering and technology Lambda Mutual recursion |
| Zdroj: | Programming Languages and Systems ISBN: 9783030341749 APLAS |
| DOI: | 10.1007/978-3-030-34175-6_10 |
| Popis: | We present new proofs—formalized in the Coq proof assistant—of the correspondence among call-by-need and (various definitions of) call-by-name evaluations of \(\lambda \)-calculus with mutually recursive bindings. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|