A functional programming approach to the specification and verification of concurrent systems

DOI10.1007/BF01887211MaRDI QIDQ909439zbMATH OpenOpenAlexFDO

Authors Peter Dybjer, Herbert P. Sander

Publication date 1989

Published in Formal Aspects of Computing (Search for Journal in Brave)

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

zbMATH Keywords

\(\mu\)- calculusalternating bit protocolfunctional programminggreatest fixed pointKahn-networksnon-deterministic processes

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Predicative specifications for functional programs describing communicating networks
• scientific article; zbMATH DE number 3903940
• scientific article; zbMATH DE number 3958712
• Formalizing process algebraic verifications in the calculus of constructions
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR

Cites work

• A refinement calculus for specifications in Hennessy-Milner logic with recursion
• Comparing integrated and external logics of functional programs
• Correspondence between ALGOL 60 and Church's Lambda-notation
• Edinburgh LCF. A mechanized logic of computation
• Finiteness is mu-ineffable
• scientific article; zbMATH DE number 3837349 (Why is no real title available?)
• scientific article; zbMATH DE number 3907752 (Why is no real title available?)
• scientific article; zbMATH DE number 4031017 (Why is no real title available?)
• scientific article; zbMATH DE number 4056971 (Why is no real title available?)
• scientific article; zbMATH DE number 3722625 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 3469994 (Why is no real title available?)
• scientific article; zbMATH DE number 3602653 (Why is no real title available?)
• scientific article; zbMATH DE number 3349291 (Why is no real title available?)
• Nondeterministic data flow programs: How to avoid the merge anomaly
• The foundation of a generic theorem prover

Cited in

(17)

• Proving the correctness of client/server software
• Realizability interpretation of coinductive definitions and program synthesis with streams
• Defining concurrent processes constructively
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• scientific article; zbMATH DE number 3898216 (Why is no real title available?)
• Functional behavior of nondeterministic and concurrent programs
• scientific article; zbMATH DE number 140005 (Why is no real title available?)
• scientific article; zbMATH DE number 1231480 (Why is no real title available?)
• scientific article; zbMATH DE number 1487742 (Why is no real title available?)
• scientific article; zbMATH DE number 3997137 (Why is no real title available?)
• scientific article; zbMATH DE number 1390334 (Why is no real title available?)
• Reasoning About Deterministic Concurrent Functional I/O
• Predicative specifications for functional programs describing communicating networks
• Programming with streams in Coq a case study: The Sieve of Eratosthenes
• Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
• A systematic approach to language constructs for concurrent programs
• A formal system for specification analysis of concurrent programs

Describes a project that uses

Uses Software

• HOL
• ALGOL 60

This page was built for publication: A functional programming approach to the specification and verification of concurrent systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q909439)