A two-valued logic for properties of strict functional programs allowing partial functions

DOI10.1007/s10817-012-9253-6zbMath1267.68088OpenAlexW2060492324MaRDI QIDQ352946

David Sabel, Manfred Schmidt-Schauss

Publication date: 5 July 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-012-9253-6

zbMATH Keywords

verificationlogicssemanticsfunctional programmingcontextual equivalence

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Related Items

Observational program calculi and the correctness of translations

Uses Software

• ACL2
• Coq
• HasCasl
• ML
• Isabelle/HOL
• HOL
• IMPS
• VeriFun
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial functions in a total setting
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A logic covering undefinedness in program proofs
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On generic context lemmas for higher-order calculi with sharing
• The connection between two ways of reasoning about partial functions
• Partial and nested recursive function definitions in higher-order logic
• HasCasl: integrated higher-order specification and program development
• The calculus of constructions
• The revised report on the syntactic theories of sequential control and state
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• A simple type theory with partial functions and subtypes
• IMPS: An interactive mathematical proof system
• Induction proofs with partial functions
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving congruence of bisimulation in functional programming languages
• Context Dependent Procedures and Computed Types in ✓eriFun
• Partial Recursive Functions in Higher-Order Logic
• A Mechanical Proof of the Unsolvability of the Halting Problem
• Proving Theorems about LISP Functions
• Adapting Calculational Logic to the Undefined
• Equivalence in functional languages with effects
• Automated Reasoning
• Reasoning About Incompletely Defined Programs
• Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
• Partiality and recursion in interactive theorem provers – an overview