A two-valued logic for properties of strict functional programs allowing partial functions
type: Item
instance of: scholarly article
title: A two-valued logic for properties of strict functional programs allowing partial functions
zbMATH Open document ID: 1267.68088
author: David Sabel
author: Manfred Schmidt-Schauß
published in: Journal of Automated Reasoning
publication date: 2013-07-05T00:00:00Z
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 6184680
zbMATH Keywords: verification
zbMATH Keywords: functional programming
zbMATH Keywords: logics
zbMATH Keywords: semantics
zbMATH Keywords: contextual equivalence
describes a project that uses: ACL2
describes a project that uses: ML
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL
describes a project that uses: Archive Formal Proofs
describes a project that uses: IMPS
describes a project that uses: Coq
describes a project that uses: HasCasl
describes a project that uses: VeriFun
MaRDI profile type: Publication
full work available at URL: s10817-012-9253-6
OpenAlex ID: W2060492324
cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY
cites work: Context dependent procedures and computed types in \texttt{VeriFun}
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: A logic covering undefinedness in program proofs
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Equivalence in functional languages with effects
cites work: Partiality and recursion in interactive theorem provers – an overview
cites work: Proving Theorems about LISP Functions
cites work: A Mechanical Proof of the Unsolvability of the Halting Problem
cites work: Partial and nested recursive function definitions in higher-order logic
cites work: Partial functions in a total setting
cites work: A simple type theory with partial functions and subtypes
cites work: The calculus of constructions
cites work: Adapting Calculational Logic to the Undefined
cites work: Automated Reasoning
cites work: IMPS: An interactive mathematical proof system
cites work: The revised report on the syntactic theories of sequential control and state
cites work: The connection between two ways of reasoning about partial functions
cites work: Induction proofs with partial functions
cites work: Q5287513
cites work: Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
cites work: Q3204055
cites work: Proving congruence of bisimulation in functional programming languages
cites work: On generic context lemmas for higher-order calculi with sharing
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
cites work: Partial Recursive Functions in Higher-Order Logic
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q4225152
cites work: Q4414725
cites work: HasCasl: integrated higher-order specification and program development
cites work: Q4296747
cites work: Reasoning About Incompletely Defined Programs
DOI: 10.1007/S10817-012-9253-6
description: scientific article; zbMATH DE number 6184680