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...

Full description

Bibliographic Details
Main Author: Sitnikovski, Boro. author (author)
Format: eBook
Language:Inglés
Published: Berkeley, CA : Apress 2023.
Edition:1st ed. 2023.
Subjects:
See on Biblioteca Universitat Ramon Llull:https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009729428606719
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.