國立高雄大學圖資館 |

Language: English

Back

Introduction to dependent types with Idrisencoding program proofs in types /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Introduction to dependent types with Idrisby Boro Sitnikovski.
Reminder of title:	encoding program proofs in types /
Author:	Sitnikovski, Boro.
Published:	Berkeley, CA :Apress :2023.
Description:	xviii, 157 p. :ill., digital ;24 cm.
Contained By:	Springer Nature eBook
Subject:	Idris (Computer program language)
Online resource:	https://doi.org/10.1007/978-1-4842-9259-4
ISBN:	9781484292594$q(electronic bk.)

Introduction to dependent types with Idrisencoding program proofs in types /
Sitnikovski, Boro.

Introduction to dependent types with Idrisencoding program proofs in types /[electronic resource] :by Boro Sitnikovski. - Berkeley, CA :Apress :2023. - xviii, 157 p. :ill., digital ;24 cm.

Chapter 1: Formal Systems -- Chapter 2: Classical Mathematical Logic -- Chapter 3: Type Theory -- Chapter 4: Programming in Idris -- Chapter 5: Proving in Idris.

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 part of the book serves as an introduction to the language's underlying theories. It starts by reviewing formal systems and mathematical logical systems as foundational building blocks, then gradually builds up to dependent types. Next, you'll learn type theory for dependent types. Following this, you'll explore the Idris programming language and conclude by exploring the depths of formal systems and type checkers by implementing them. Introduction to Dependent Types with Idris will walk you through simple examples through more advanced techniques, stepping up the difficulty as you gain more knowledge. Every chapter includes a set of exercises based on what it covered to further cement your learning. No specialized knowledge of mathematics is expected beyond the basics, so it is perfect for novices. You will: Understand Lambda calculus and dependent types Gain insight into functional programming Write mathematical proofs with Idris.

ISBN: 9781484292594$q(electronic bk.)

Standard No.: 10.1007/978-1-4842-9259-4doiSubjects--Topical Terms:

951542
Idris (Computer program language)

LC Class. No.: QA76.62

Dewey Class. No.: 005.114

Introduction to dependent types with Idrisencoding program proofs in types /
LDR:02423nmm a2200325 a 4500 001 643672
003 DE-He213
005 20230317070505.0
006 m d
007 cr nn 008maaau
008 231123s2023 cau s 0 eng d
020 $a 9781484292594$q(electronic bk.)
020 $a 9781484292587$q(paper)
024 7 $a 10.1007/978-1-4842-9259-4 $2 doi
035 $a 978-1-4842-9259-4
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.62
072 7 $a UMX $2 bicssc
072 7 $a COM000000 $2 bisacsh
072 7 $a UMX $2 thema
082 0 4 $a 005.114 $2 23
090 $a QA76.62 $b .S623 2023
100 1 $a Sitnikovski, Boro. $3 891745
245 1 0 $a Introduction to dependent types with Idris $h [electronic resource] : $b encoding program proofs in types / $c by Boro Sitnikovski.
260 $a Berkeley, CA : $b Apress : $b Imprint: Apress, $c 2023.
300 $a xviii, 157 p. : $b ill., digital ; $c 24 cm.
505 0 $a Chapter 1: Formal Systems -- Chapter 2: Classical Mathematical Logic -- Chapter 3: Type Theory -- Chapter 4: Programming in Idris -- Chapter 5: Proving in Idris.
520 $a 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 part of the book serves as an introduction to the language's underlying theories. It starts by reviewing formal systems and mathematical logical systems as foundational building blocks, then gradually builds up to dependent types. Next, you'll learn type theory for dependent types. Following this, you'll explore the Idris programming language and conclude by exploring the depths of formal systems and type checkers by implementing them. Introduction to Dependent Types with Idris will walk you through simple examples through more advanced techniques, stepping up the difficulty as you gain more knowledge. Every chapter includes a set of exercises based on what it covered to further cement your learning. No specialized knowledge of mathematics is expected beyond the basics, so it is perfect for novices. You will: Understand Lambda calculus and dependent types Gain insight into functional programming Write mathematical proofs with Idris.
650 0 $a Idris (Computer program language) $3 951542
650 0 $a Functional programming (Computer science) $3 277879
650 1 4 $a Programming Language. $3 913494
650 2 4 $a Software Engineering. $3 274511
710 2 $a SpringerLink (Online service) $3 273601
773 0 $t Springer Nature eBook
856 4 0 $u https://doi.org/10.1007/978-1-4842-9259-4
950 $a Professional and Applied Computing (SpringerNature-12059)