語系:
繁體中文
English
說明(常見問題)
回圖書館首頁
手機版館藏查詢
登入
回首頁
切換:
標籤
|
MARC模式
|
ISBD
Introduction to dependent types with...
~
Sitnikovski, Boro.
FindBook
Google Book
Amazon
博客來
Introduction to dependent types with Idris = encoding program proofs in types /
紀錄類型:
書目-電子資源 : Monograph/item
正題名/作者:
Introduction to dependent types with Idris/ by Boro Sitnikovski.
其他題名:
encoding program proofs in types /
作者:
Sitnikovski, Boro.
出版者:
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.
Contained By:
Springer Nature eBook
標題:
Idris (Computer program language) -
電子資源:
https://doi.org/10.1007/978-1-4842-9259-4
ISBN:
9781484292594
Introduction to dependent types with Idris = encoding program proofs in types /
Sitnikovski, Boro.
Introduction to dependent types with Idris
encoding 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
Standard No.: 10.1007/978-1-4842-9259-4doiSubjects--Topical Terms:
3632897
Idris (Computer program language)
LC Class. No.: QA76.62
Dewey Class. No.: 005.114
Introduction to dependent types with Idris = encoding program proofs in types /
LDR
:02423nmm a2200325 a 4500
001
2318143
003
DE-He213
005
20230317070505.0
006
m d
007
cr nn 008maaau
008
230902s2023 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
3495014
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
3632897
650
0
$a
Functional programming (Computer science)
$3
524481
650
1 4
$a
Programming Language.
$3
3538935
650
2 4
$a
Software Engineering.
$3
890874
710
2
$a
SpringerLink (Online service)
$3
836513
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)
筆 0 讀者評論
館藏地:
全部
電子資源
出版年:
卷號:
館藏
1 筆 • 頁數 1 •
1
條碼號
典藏地名稱
館藏流通類別
資料類型
索書號
使用類型
借閱狀態
預約狀態
備註欄
附件
W9454393
電子資源
11.線上閱覽_V
電子書
EB QA76.62
一般使用(Normal)
在架
0
1 筆 • 頁數 1 •
1
多媒體
評論
新增評論
分享你的心得
Export
取書館
處理中
...
變更密碼
登入