scientific article; zbMATH DE number 1420794
From MaRDI portal
Publication:4944858
zbMath0942.03014MaRDI QIDQ4944858
Carsten Schuermann, Frank Pfenning
Publication date: 22 March 2000
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
dependently typed \(\lambda\)-calculusinteraction of notational definitions with algorithms for testing equality and unification
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items (6)
A canonical locally named representation of binding ⋮ Logical approximation for program analysis ⋮ Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ⋮ Automated techniques for provably safe mobile code. ⋮ Redundancy Elimination for LF ⋮ Reducing higher-order theorem proving to a sequence of SAT problems
Uses Software
This page was built for publication:
