Introduction to Dependent Types with Idris Encoding Program Proofs in Types
Dependent types are a concept that allows developers to write proof-carrying code. Idris is a programming language that supports dependent types. This book will teach you the mathematical foundations of Idris as well as how to use it to write software and mathematically prove properties. The first p...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berkeley, CA
Apress
2023, 2023
|
| Edition: | 1st ed. 2023 |
| Subjects: | |
| Online Access: | |
| Collection: | Springer eBooks 2005- - Collection details see MPG.ReNa |
Table of Contents:
- Chapter 1: Formal Systems
- Chapter 2: Classical Mathematical Logic
- Chapter 3: Type Theory
- Chapter 4: Programming in Idris
- Chapter 5: Proving in Idris