A two-valued logic for properties of strict functional programs allowing partial functions
From MaRDI portal
Publication:352946
DOI10.1007/S10817-012-9253-6zbMATH Open1267.68088OpenAlexW2060492324MaRDI QIDQ352946FDOQ352946
Authors: David Sabel, Manfred Schmidt-Schauß 
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
Recommendations
Cites Work
- HasCasl: integrated higher-order specification and program development
- Title not available (Why is that?)
- IMPS: An interactive mathematical proof system
- Reasoning About Incompletely Defined Programs
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Isabelle/HOL. A proof assistant for higher-order logic
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The revised report on the syntactic theories of sequential control and state
- Proving congruence of bisimulation in functional programming languages
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Title not available (Why is that?)
- Partiality and recursion in interactive theorem provers -- an overview
- A logic covering undefinedness in program proofs
- The calculus of constructions
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- A simple type theory with partial functions and subtypes
- Induction proofs with partial functions
- Context dependent procedures and computed types in \texttt{VeriFun}
- Title not available (Why is that?)
- Partial Recursive Functions in Higher-Order Logic
- A Mechanical Proof of the Unsolvability of the Halting Problem
- Proving Theorems about LISP Functions
- Title not available (Why is that?)
- Adapting Calculational Logic to the Undefined
- Title not available (Why is that?)
- Equivalence in functional languages with effects
- Automated Reasoning
- Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
- Partial functions in a total setting
- 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
Cited In (4)
Uses Software
This page was built for publication: A two-valued logic for properties of strict functional programs allowing partial functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352946)
