Úvod do závislých typů s Idrisem: Kódování důkazů programů v typech

Recenze čtenářů

Aktuálně nejsou k dispozici žádné recenze čtenářů. Hodnocení je založeno na 2 hlasů.

Původní název:

Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

Obsah knihy:

Závislé typy jsou konceptem, který vývojářům umožňuje psát kód nesoucí důkazy. Idris je programovací jazyk, který podporuje závislé typy. V této knize se naučíte matematické základy Idrisu i to, jak jej používat k psaní softwaru a matematickému dokazování vlastností.

První část knihy slouží jako úvod do základních teorií jazyka. Začíná přehledem formálních systémů a matematických logických systémů jako základních stavebních kamenů a postupně přechází k závislým typům. Dále se seznámíte s teorií typů pro závislé typy. Následně se seznámíte s programovacím jazykem Idris a na závěr prozkoumáte hloubku formálních systémů a kontrolorů typů jejich implementací.

Úvod do závislých typů s Idrisem vás provede jednoduchými příklady až po pokročilejší techniky, přičemž s přibývajícími znalostmi se obtížnost stupňuje. Každá kapitola obsahuje sadu cvičení založených na tom, co se v ní probíralo, abyste si učení ještě více upevnili. Nad rámec základů se neočekávají žádné specializované znalosti matematiky, takže je ideální pro začátečníky.

Co se naučíte

Porozumět lambda kalkulu a závislým typům.

⬤ Získat přehled o funkcionálním programování.

⬤ Pište matematické důkazy s Idrisem.

Pro koho je tato kniha určena

Programátorům, matematikům, akademickým pracovníkům a všem, kteří mají zájem naučit se závislé typy a lambda kalkul.