NASA NTRS · 19990116988
Dependent Types and Explicit Substitutions
Abstract
We present a dependent-type system for a lambda-calculus with explicit substitutions. In this system, meta-variables, subject reduction, soundness, confluence and weak normalization.
Keep this discovery
Explore connections, maps & timelines
Munoz, Ceasar. 1999-11-01. Dependent Types and Explicit Substitutions. https://ntrs.nasa.gov/citations/19990116988
Cite the original work for its findings. Save a collection to share your selection of sources.