Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Sixth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {191--202},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski