Building reliable, high-performance networks with the Nuprl proof development system

DOI10.1017/S0956796803004854MaRDI QIDQ4819652zbMATH OpenFDO

Authors Christoph Kreitz

Publication date 27 September 2004

Published in Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• Formal program optimization in Nuprl using computational equivalence and partial types
• scientific article; zbMATH DE number 140008
• scientific article; zbMATH DE number 3903940
• Computational verification of network programs in Coq
• Towards a formally verified proof assistant

Cited in

(4)

• Adapting functional programs to higher order logic
• Formal program optimization in Nuprl using computational equivalence and partial types
• Innovations in computational type theory using Nuprl
• Constructive membership predicates as index types

Describes a project that uses

Uses Software

• Specware
• LOOP
• JProver
• Twelf
• Nuprl
• OCaml
• MetaPRL
• JML
• PVS
• TPS
• Coq

This page was built for publication: Building reliable, high-performance networks with the Nuprl proof development system

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