Using Untypes Lambda Calculus to Computer with Atoms
Axioms and verification rules are given for typeless A -calculus with a conditional test for equality between atoms. A semantic completeness theorem is proved and a deterministic evaluator is proposed.
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149598 |
| Summary: | Axioms and verification rules are given for typeless A -calculus with a conditional test for equality between atoms. A semantic completeness theorem is proved and a deterministic evaluator is proposed. |
|---|