A typed logic of partial functions reconstructed classically

DOI10.1007/BF01178666zbMath0804.03018OpenAlexW2030221869MaRDI QIDQ1338893

V. Pereyra

Publication date: 24 January 1995

Published in: Acta Informatica (Search for Journal in Brave)

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

zbMATH Keywords

formal specificationembeddings into classical infinitary logiclogic LPFsoftware development method VDMverified design

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (12)

1998 European Summer Meeting of the Association for Symbolic Logic ⋮ Non-deterministic expressions and predicate transformers ⋮ Kleene's three-valued logic and process algebra ⋮ Are the logical foundations of verifying compiler prototypes matching user expectations? ⋮ Empowering the Event-B method using external theories ⋮ Partial arithmetical data types of rational numbers and their equational specification ⋮ Truth versus information in logic programming ⋮ A completeness proof for a regular predicate logic with undefined truth value ⋮ Partial functions and logics: A warning ⋮ Model-Checking View-Based Partial Specifications ⋮ The connection between two ways of reasoning about partial functions ⋮ Process algebra with four-valued logic

Cites Work

• A logic covering undefinedness in program proofs
• Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
• Unnamed Item

This page was built for publication: A typed logic of partial functions reconstructed classically