1 citations · 1 across the 2 of their papers we have counts for
2 papers
cs.LO2026
An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus
Rob Nederpelt, Ferruccio Guidi
Terms in the lambda-calculus can be represented as planar trees decorated with symbols for abstraction and application, and having variables as leaves. In this paper, we concentrat…
cs.LO2022★ 1 cited
Characteristics of de Bruijn's early proof checker Automath
Herman Geuvers, Rob Nederpelt
The `mathematical language' Automath, conceived by N.G. de Bruijn in 1968, was the first theorem prover actually working and was used for checking many specimina of mathematical co…