Explicit Substitutions and All That

Abstract

Explicit substitution calculi are extensions of the lambda-calculus where the substitution mechanism is internalized into the theory. This feature makes them suitable for implementation and theoretical study of logic-based tools such as strongly typed programming languages and proof assistant systems. In this paper we explore new developments on two of the most successful styles of explicit substitution calculi: the lambda sigma- and lambda S(e)-calculi.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 2000
Accession Number
ADA385383

Entities

People

  • Cesar Munoz
  • Mauricio Ayala-rincon

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Calculus
  • Computations
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Equations
  • Formal Languages
  • Judgment
  • Language
  • Mathematics
  • Notation
  • Numbers
  • Programming Languages
  • Theoretical Computer Science

Readers

  • Computational Linguistics