scientific article; zbMATH DE number 512774

zbMath0788.68015MaRDI QIDQ4281467

Ulrich Berger

Publication date: 15 May 1994

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

typed lambda-calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40)

Related Items (17)

Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ Algebraic proofs of cut elimination ⋮ Towards the computational complexity of \(\mathcal{PR}^ \omega\)-terms ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Unnamed Item ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Higman’s Lemma and Its Computational Content ⋮ Two different strong normalization proofs? ⋮ An arithmetic for polynomial-time computation ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Realizability interpretation of proofs in constructive analysis ⋮ An arithmetic for non-size-increasing polynomial-time computation ⋮ The Simple Type Theory of Normalisation by Evaluation ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Program extraction from normalization proofs

This page was built for publication: