Logo

Certified Programming with Dependent Types

Small book cover: Certified Programming with Dependent Types

Certified Programming with Dependent Types
by


Number of pages: 371

Description:
Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits. The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science.

Home page url

Download or read it online for free here:
Download link
(3.9MB, PDF)

Similar books

Book cover: Professor Frisby's Mostly Adequate Guide to Functional ProgrammingProfessor Frisby's Mostly Adequate Guide to Functional Programming
- GitBook
This is a book on the functional paradigm in general. We will use the world's most popular functional programming language: JavaScript. JavaScript will be our means of learning a paradigm, where you apply it is up to you.
(4110 views)
Book cover: The Design of Functional Programs - A Calculational ApproachThe Design of Functional Programs - A Calculational Approach
by - Technische Universiteit Eindhoven
This document was started as a research to what extent functional programs can be designed in a calculational way. This should be possible because functional-program notations carry less operational connotations than their sequential counterparts do.
(7969 views)
Book cover: Programming in Standard MLProgramming in Standard ML
by - Carnegie Mellon University
Introduction to programming with the Standard ML - a formally defined programming language. The text covers the core language, declarations, functions, products and records, recursive functions, type inference and polymorphism, lists, and more.
(8528 views)
Book cover: A Gentle Introduction to MLA Gentle Introduction to ML
by - Napier University
Functional languages such as ML, Hope and Lisp allow us to develop programs which will submit logical analysis relatively easily. Using a functional language we can make assertions about programs and prove these assertions to be correct.
(6354 views)