A two-valued logic for properties of strict functional programs allowing partial functions
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4180818 (Why is no real title available?)
- scientific article; zbMATH DE number 1241702 (Why is no real title available?)
- scientific article; zbMATH DE number 592368 (Why is no real title available?)
- scientific article; zbMATH DE number 1953273 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A Mechanical Proof of the Unsolvability of the Halting Problem
- A logic covering undefinedness in program proofs
- A simple type theory with partial functions and subtypes
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Adapting Calculational Logic to the Undefined
- Automated Reasoning
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Context dependent procedures and computed types in \texttt{VeriFun}
- Equivalence in functional languages with effects
- HasCasl: integrated higher-order specification and program development
- IMPS: An interactive mathematical proof system
- Induction proofs with partial functions
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
- On generic context lemmas for higher-order calculi with sharing
- Partial Recursive Functions in Higher-Order Logic
- Partial and nested recursive function definitions in higher-order logic
- Partial functions in a total setting
- Partiality and recursion in interactive theorem provers -- an overview
- Proving Theorems about LISP Functions
- Proving congruence of bisimulation in functional programming languages
- Reasoning About Incompletely Defined Programs
- The calculus of constructions
- The connection between two ways of reasoning about partial functions
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The revised report on the syntactic theories of sequential control and state
Cited in
(4)
Describes a project that uses
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)
