Pruning simply typed -terms

DOI10.1093/logcom/6.5.663zbMath0863.03007OpenAlexW2131558630MaRDI QIDQ4716047

Stefano Berardi

Publication date: 3 June 1997

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/6.5.663

zbMATH Keywords

complexityalgorithmtypespruningprogram extractionlambda-calculusobservational equivalence

Mathematics Subject Classification ID

Logic in computer science (03B70) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Getting results from programs extracted from classical proofs ⋮ Extracting functional programs from Coq, in Coq ⋮ System ST toward a type system for extraction and proofs of programs ⋮ Unnamed Item ⋮ First order marked types ⋮ Towards the animation of proofs -- testing proofs by examples ⋮ Refinement types for program analysis

This page was built for publication: Pruning simply typed  -terms