| 000 | 03500nam a2200565 i 4500 | ||
|---|---|---|---|
| 001 | 8681597 | ||
| 003 | IEEE | ||
| 005 | 20220712204937.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 190417s2019 mau ob 001 eng d | ||
| 020 |
_a9780262355469 _qelectronic bk. |
||
| 020 | _z9780262536431 | ||
| 035 | _a(CaBNVSL)mat08681597 | ||
| 035 | _a(IDAMS)0b00006488f61543 | ||
| 040 |
_aCaBNVSL _beng _erda _cCaBNVSL _dCaBNVSL |
||
| 050 | 4 |
_aQA76.63 _b.F75 2018eb |
|
| 082 | 0 | 4 |
_a005.101/5113 _223 |
| 100 | 1 |
_aFriedman, Daniel P., _eauthor. _922920 |
|
| 245 | 1 | 4 |
_aThe little typer / _cDaniel P. Friedman, David Thrane Christiansen ; drawings by Duane Bibby ; foreword by Robert Harper ; afterword by Conor McBride. |
| 264 | 1 |
_aCambridge : _bMIT Press, _c2018. |
|
| 264 | 2 |
_a[Piscataqay, New Jersey] : _bIEEE Xplore, _c[2019] |
|
| 300 | _a1 PDF (424 pages). | ||
| 336 |
_atext _2rdacontent |
||
| 337 |
_aelectronic _2isbdmedia |
||
| 338 |
_aonline resource _2rdacarrier |
||
| 506 | _aRestricted to subscribers or individual electronic text purchasers. | ||
| 520 | _aAn introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. A program's type describes its behavior. Dependent types are a first-class part of a language, and are much more powerful than other kinds of types; using just one language for types and programs allows program descriptions to be as powerful as the programs they describe. The Little Typer explains dependent types, beginning with a very small language that looks very much like Scheme and extending it to cover both programming with dependent types and using dependent types for mathematical reasoning. Readers should be familiar with the basics of a Lisp-like programming language, as presented in the first four chapters of The Little Schemer . The first five chapters of The Little Typer provide the needed tools to understand dependent types; the remaining chapters use these tools to build a bridge between mathematics and programming. Readers will learn that tools they know from programming--pairs, lists, functions, and recursion--can also capture patterns of reasoning. The Little Typer does not attempt to teach either practical programming skills or a fully rigorous approach to types. Instead, it demonstrates the most beautiful aspects as simply as possible, one step at a time. | ||
| 530 | _aAlso available in print. | ||
| 538 | _aMode of access: World Wide Web | ||
| 588 | 0 | _aPrint version record. | |
| 650 | 0 |
_aFunctional programming (Computer science) _921993 |
|
| 650 | 0 |
_aLogic programming. _92730 |
|
| 650 | 0 |
_aComputer logic. _922599 |
|
| 650 | 0 |
_aType theory. _925645 |
|
| 650 | 7 |
_aComputer logic. _2fast _922599 |
|
| 650 | 7 |
_aFunctional programming (Computer science) _2fast _921993 |
|
| 650 | 7 |
_aLogic programming. _2fast _92730 |
|
| 650 | 7 |
_aType theory. _2fast _925645 |
|
| 655 | 4 |
_aElectronic books. _93294 |
|
| 700 | 1 |
_aChristiansen, David Thrane, _eauthor. _925646 |
|
| 700 | 1 |
_aBibby, Duane, _eillustrator. _925647 |
|
| 700 | 1 |
_aHarper, Robert, _d1957- _925648 |
|
| 700 | 1 |
_aMcBride, Conor. _925649 |
|
| 710 | 2 |
_aIEEE Xplore (Online Service), _edistributor. _925650 |
|
| 710 | 2 |
_aMIT Press, _epublisher. _925651 |
|
| 776 | 0 | 8 |
_iPrint version: _aFriedman, Daniel P., author. _tLittle typer _z9780262536431 _w(DLC) 2018017792 _w(OCoLC)1030596012 |
| 856 | 4 | 2 |
_3Abstract with links to resource _uhttps://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=8681597 |
| 942 | _cEBK | ||
| 999 |
_c73595 _d73595 |
||