Logic in Computer Science (LICS 1991)

Paper: Equational programming in λ-calculus (at LICS 1991)

Authors: Enrico Tronci

Abstract

A system of equations in λ-calculus is a pair (Γ, X) where Γ is a set of formulas of Λ (the equations) and X is a finite set of variables of Λ (the unknowns). A system S=(Γ, X) is said to be solvable in the theory T (T-solvable) if there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the formulas of Γ theorems in the theory T. A class of systems for which the β-solvability problem is decidable in polynomial time is defined. This class yields an equational programming language in which constraints on the code generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way

BibTeX

  @InProceedings{Tronci-Equationalprogrammi,
    author = 	 {Enrico Tronci},
    title = 	 {Equational programming in λ-calculus},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {191--202},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }