A complete and decidable proof system for call-by-value equalities

DOI10.1007/BFB0032019MaRDI QIDQ4038678zbMATH OpenFDO

Authors Jon G. Riecke

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0032019

zbMATH Keywords

call-by-value observational congruencesfunctional languagesprogramming language for computable functions

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A formal equational theory for call-by-push-value
• A language-independent proof system for full program equivalence
• Sound and complete axiomatisations of call-by-value control operators
• Polymorphic call-by-value calculus based on classical proofs (extended abstract)
• Call-by-value solvability, revisited
• Proof nets and the call-by-value \(\lambda\)-calculus
• scientific article; zbMATH DE number 7356671
• Call-by-value separability and computability
• A Semantical and Operational Account of Call-by-Value Solvability

Cited in

(5)

• System \(T\), call-by-value and the minimum problem
• A formal equational theory for call-by-push-value
• An abstract machine for strong call by value
• Call-by-value lambda calculus as a model of computation in Coq
• Extended call-by-push-value: reasoning about effectful programs and evaluation order

Describes a project that uses

Uses Software

• LISP

This page was built for publication: A complete and decidable proof system for call-by-value equalities

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4038678)