MARC details
| 000 -LEADER |
|---|
| fixed length control field |
06774cam a2200433 i 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
17778322 |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20201015140903.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
130614t20142014njua 001 0 eng |
| 010 ## - LIBRARY OF CONGRESS CONTROL NUMBER |
|---|
| LC control number |
2013020038 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9781118007471 (pbk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
1118007476 (pbk.) |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
DLC |
| Language of cataloging |
eng |
| Transcribing agency |
DLC |
| Description conventions |
rda |
| Modifying agency |
DLC |
| -- |
EG-NcFUE |
| 042 ## - AUTHENTICATION CODE |
|---|
| Authentication code |
pcc |
| 050 00 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.7 |
| Item number |
.S84 2014 |
| 082 00 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.1 |
| Edition number |
23 |
| Item number |
S.A.P |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
COM051230 |
| Source of number |
bisacsh |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Stump, Aaron, |
| Relator term |
author. |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Programming language foundations / |
| Statement of responsibility, etc |
Aaron Stump, Department of Computer Science, University of Iowa. |
| 250 ## - EDITION STATEMENT |
|---|
| Edition statement |
First edition. |
| 264 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc |
Hoboken, NJ : |
| Name of publisher, distributor, etc |
Wiley, |
| Date of publication, distribution, etc |
[2014] |
| 264 #4 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Date of publication, distribution, etc |
©2014 |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
x, 326 pages : |
| Other physical details |
illustrations ; |
| Dimensions |
24 cm |
| 336 ## - CONTENT TYPE |
|---|
| Content type term |
text |
| Source |
rdacontent |
| 337 ## - MEDIA TYPE |
|---|
| Media type term |
unmediated |
| Source |
rdamedia |
| 338 ## - CARRIER TYPE |
|---|
| Carrier type term |
volume |
| Source |
rdacarrier |
| 500 ## - GENERAL NOTE |
|---|
| General note |
computer bookfair2015 |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references (pages 321-323) and index. |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
I Central Topics 7<br/><br/>1 Semantics of First-Order Arithmetic 9<br/><br/>1.1 Syntax of FO(Z) terms 10<br/><br/>1.2 Informal semantics of FO(Z) terms 10<br/><br/>1.3 Syntax of FO(Z) formulas 11<br/><br/>1.4 Some alternative logical languages for arithmetic 12<br/><br/>1.5 Informal semantics of FO(Z) formulas 13<br/><br/>1.6 Formal semantics of FO(Z) terms 14<br/><br/>1.6.1 Examples 17<br/><br/>1.7 Formal semantics of FO(Z) formulas 18<br/><br/>1.7.1 Examples 18<br/><br/>1.8 Compositionality 19<br/><br/>1.9 Validity and satisfiability 19<br/><br/>1.10 Interlude: proof by natural-number induction 20<br/><br/>1.11 Proof by structural induction 27<br/><br/>1.12 Conclusion 28<br/><br/>1.13 Basic exercises 29<br/><br/>1.14 Intermediate exercises 30<br/><br/>2 Denotational Semantics of WHILE 33<br/><br/>2.1 Syntax and informal semantics of WHILE 33<br/><br/>2.2 Beginning of the formal semantics for WHILE 34<br/><br/>2.3 Problem with the semantics of while-commands 35<br/><br/>2.4 Domains 37<br/><br/>2.5 Continuous functions 42<br/><br/>2.6 The least fixed-point theorem 46<br/><br/>2.7 Completing the formal semantics of commands 48<br/><br/>2.8 Connection to practice: static analysis using abstract interpretation 54<br/><br/>2.9 Conclusion 59<br/><br/>2.10 Basic exercises 60<br/><br/>2.11 Intermediate exercises 62<br/><br/>3 Axiomatic Semantics of WHILE 65<br/><br/>3.1 Denotational equivalence 66<br/><br/>3.2 Partial correctness assertions 68<br/><br/>3.3 Interlude: rules and derivations 71<br/><br/>3.4 Hoare Logic rules 76<br/><br/>3.5 Example derivations in Hoare Logic 82<br/><br/>3.6 Soundness of Hoare Logic and induction on the structure of derivations 87<br/><br/>3.7 Conclusion 92<br/><br/>3.8 Exercises 92<br/><br/>4 Operational Semantics of WHILE 95<br/><br/>4.1 Big-step semantics of WHILE 95<br/><br/>4.2 Small-step semantics of WHILE 97<br/><br/>4.3 Relating the two operational semantics 101<br/><br/>4.4 Conclusion 120<br/><br/>4.5 Basic exercises 120<br/><br/>4.6 Intermediate exercises 122<br/><br/>5 Untyped Lambda Calculus 125<br/><br/>5.1 Abstract syntax of untyped lambda calculus 125<br/><br/>5.2 Operational semantics: full b-reduction 127<br/><br/>5.3 Defining full b-reduction with contexts 132<br/><br/>5.4 Specifying other reduction orders with contexts 134<br/><br/>5.5 Big-step call-by-value operational semantics 137<br/><br/>5.6 Relating big-step and small-step operational semantics 138<br/><br/>5.7 Conclusion 142<br/><br/>5.8 Basic Exercises 143<br/><br/>5.9 Intermediate Exercises 147<br/><br/>5.10 More Challenging Exercises 147<br/><br/>6 Programming in Untyped Lambda Calculus 149<br/><br/>6.1 The Church encoding for datatypes 149<br/><br/>6.2 The Scott encoding for datatypes 156<br/><br/>6.3 Other datatypes: lists 158<br/><br/>6.4 Non-recursive operations on Scott-encoded data 158<br/><br/>6.5 Recursive equations and the fix operator 160<br/><br/>6.6 Another recursive example: multiplication 162<br/><br/>6.7 Conclusion 162<br/><br/>6.8 Basic exercises 163<br/><br/>6.9 Intermediate exercises 164<br/><br/>7 Simple Type Theory 167<br/><br/>7.1 Abstract syntax of simple type theory 167<br/><br/>7.2 Semantics of types 168<br/><br/>7.3 Type-assignment rules 169<br/><br/>7.4 Semantic soundness for type-assignment rules 169<br/><br/>7.5 Applying semantic soundness to prove normalization 171<br/><br/>7.6 Type preservation 173<br/><br/>7.7 The Curry-Howard isomorphism 176<br/><br/>7.8 Algorithmic typing 183<br/><br/>7.9 Algorithmic typing via constraint generation 186<br/><br/>7.10 Subtyping 190<br/><br/>7.11 Conclusion 199<br/><br/>7.12 Basic Exercises 200<br/><br/>7.13 Intermediate Exercises 202<br/><br/>II Extra Topics 205<br/><br/>8 Nondeterminism and Concurrency 207<br/><br/>8.1 Guarded commands 207<br/><br/>8.2 Operational semantics of guarded commands 208<br/><br/>8.3 Concurrent WHILE 215<br/><br/>8.4 Operational semantics of concurrent WHILE 216<br/><br/>8.5 Milner’s Calculus of Communicating Systems 219<br/><br/>8.6 Operational semantics of CCS 220<br/><br/>8.7 Conclusion 226<br/><br/>8.8 Basic exercises 226<br/><br/>8.9 Intermediate exercises 228<br/><br/>9 More on Untyped Lambda Calculus 231<br/><br/>9.1 Confluence of untyped lambda calculus 231<br/><br/>9.2 Combinators 259<br/><br/>9.3 Conclusion 266<br/><br/>9.4 Basic exercises 266<br/><br/>9.5 Intermediate exercises 267<br/><br/>10 Polymorphic Type Theory 269<br/><br/>10.1 Type-assignment version of System F 269<br/><br/>10.2 Annotated terms for System F 271<br/><br/>10.3 Semantics of annotated System F 272<br/><br/>10.4 Programming with Church-encoded data 274<br/><br/>10.5 Higher-kind polymorphism and System Fw 276<br/><br/>10.6 Conclusion 283<br/><br/>10.7 Exercises 283<br/><br/>11 Functional Programming 285<br/><br/>11.1 Call-by-value functional programming 286<br/><br/>11.2 Connection to practice: eager FP in OCaml<br/><br/>11.3 Lazy programming with call-by-name evaluation 300<br/><br/>11.4 Connection to practice: lazy FP in Haskell 304<br/><br/>11.5 Conclusion 310<br/><br/>11.6 Basic Exercises 310<br/><br/>11.7 Intermediate exercises 312<br/><br/>Mathematical Background 315<br/><br/>Bibliography 321 |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc |
"Stump's Programming Language Foundations is a short concise text that covers semantics, equally weighting operational and denotational semantics for several different programming paradigms: imperative, concurrent, and functional. Programming Language Foundations provides: an even coverage of denotational, operational an axiomatic semantics; extensions to concurrent and non-deterministic versions; operational semantics for untyped lambda calculus; functional programming; type systems; and coverage of emerging topics and modern research directions. "-- |
| Assigning source |
Provided by publisher. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Programming languages (Electronic computers) |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Programming languages (Electronic computers) |
| General subdivision |
Semantics. |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
COMPUTERS / Software Development & Engineering / General. |
| Source of heading or term |
bisacsh |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Display text |
Online version: |
| Main entry heading |
Stump, Aaron. |
| Title |
Programming language foundations |
| Edition |
First edition. |
| Place, publisher, and date of publication |
Hoboken, [New Jersey] : John Wiley & Sons, Inc., [2013] |
| International Standard Book Number |
9781118476840 |
| Record control number |
(DLC) 2013024641 |
| 856 ## - ELECTRONIC LOCATION AND ACCESS |
|---|
| Materials specified |
Abstract |
| Uniform Resource Identifier |
<a href="http://repository.fue.edu.eg/xmlui/handle/123456789/3600">http://repository.fue.edu.eg/xmlui/handle/123456789/3600</a> |
| 906 ## - LOCAL DATA ELEMENT F, LDF (RLIN) |
|---|
| a |
7 |
| b |
cbc |
| c |
orignew |
| d |
1 |
| e |
ecip |
| f |
20 |
| g |
y-gencatlg |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Source of classification or shelving scheme |
Dewey Decimal Classification |
| Koha item type |
Books |