Karim Nour ; Khelifa Saber - The call-by-value λµ∧∨-calculus

dmtcs:3470 - Discrete Mathematics & Theoretical Computer Science, January 1, 2005, DMTCS Proceedings vol. AF, Computational Logic and Applications (CLA '05) - https://doi.org/10.46298/dmtcs.3470
The call-by-value λµ∧∨-calculus

Authors: Karim Nour 1; Khelifa Saber 1

  • 1 Laboratoire de Mathématiques

In this paper, we introduce the $λ μ ^{∧∨}$ - call-by-value calculus and we give a proof of the Church-Rosser property of this system. This proof is an adaptation of that of Andou (2003) which uses an extended parallel reduction method and complete development.

Volume: DMTCS Proceedings vol. AF, Computational Logic and Applications (CLA '05)
Section: Proceedings
Published on: January 1, 2005
Imported on: May 10, 2017
Keywords: Call-by-value,Propositional classical logic,Parallel reduction,Complete development,Church-Rosser,[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO],[INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC]

Linked publications - datasets - softwares

Source : ScholeXplorer IsRelatedTo DOI 10.1016/s0304-3975(99)00178-4
  • 10.1016/s0304-3975(99)00178-4
On the intuitionistic force of classical search

Consultation statistics

This page has been seen 133 times.
This article's PDF has been downloaded 129 times.