A short proof of the lexical addressing algorithm

DOI10.1016/0020-0190(90)90165-TzbMath0704.68078OpenAlexW1969998283MaRDI QIDQ917326

Mitchell Wand

Publication date: 1990

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(90)90165-t

zbMATH Keywords

formal semanticsprogramming calculiChurch codingcompiler correctness proofsdeBruijn codingenvironment codingFrege codinglexical address codingnatural coding

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Correctness of procedure representations in higher-order assembly language

Uses Software

• mini-ML

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Deriving Target Code as a Representation of Continuation Semantics
• Unnamed Item
• Unnamed Item
• Unnamed Item