scientific article; zbMATH DE number 683368

MaRDI QIDQ4312490zbMATH OpenFDO

Authors M. P. A. Sellink

Publication date 8 November 1994

zbMATH Keywords

\(\lambda\)-calculusautomatic verificationprocess algebra

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formalizing process algebraic verifications in the calculus of constructions
• scientific article; zbMATH DE number 1555176
• scientific article; zbMATH DE number 1231633
• -calculus in (Co)inductive-type theory
• scientific article; zbMATH DE number 1082078

Cited in

(11)

• Formalizing process algebraic verifications in the calculus of constructions
• Formal verification of a leader election protocol in process algebra
• Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
• Proof assistance for refinement in type theory
• scientific article; zbMATH DE number 1555176 (Why is no real title available?)
• Size-based termination of higher-order rewriting
• An application of co-inductive types in Coq: verification of the alternating bit protocol
• Efficient Verified Programs in a Type Theory with Mixed Constructivity
• scientific article; zbMATH DE number 5181778 (Why is no real title available?)
• Inductive-data-type systems
• Confluence for process verification

Describes a project that uses

Uses Software

• Nuprl
• Coq

This page was built for publication:

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