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

DOI10.1017/S0956796803004854zbMATH Open1083.68010MaRDI QIDQ4819652FDOQ4819652

Christoph Kreitz

Publication date: 27 September 2004

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

Recommendations

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

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)

Cited In (3)

• Adapting functional programs to higher order logic
• Innovations in computational type theory using Nuprl
• Constructive membership predicates as index types

Uses Software

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

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)