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

DOI10.1007/BF01887211zbMath0694.68015OpenAlexW3015550054MaRDI QIDQ909439

Herbert P. Sander, Peter Dybjer

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

functional programmingalternating bit protocolnon-deterministic processes\(\mu\)- calculusgreatest fixed pointKahn-networks

Mathematics Subject Classification ID

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

Related Items (4)

Programming with streams in Coq a case study: The Sieve of Eratosthenes ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Realizability interpretation of coinductive definitions and program synthesis with streams ⋮ Defining concurrent processes constructively

Uses Software

• HOL
• ALGOL 60

Cites Work

• A refinement calculus for specifications in Hennessy-Milner logic with recursion
• Comparing integrated and external logics of functional programs
• Nondeterministic data flow programs: How to avoid the merge anomaly
• Finiteness is mu-ineffable
• Edinburgh LCF. A mechanized logic of computation
• The foundation of a generic theorem prover
• Correspondence between ALGOL 60 and Church's Lambda-notation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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