This book is about beliefs---how we get them and how we evaluate them. It takes the form of a fictional conversation makes the following points: 1) in analogy with robots, we humans know by the models we make of reality, 2) these models are always provisional and sometimes unreliable, 3) it is especially important to examine thoroughly those models upon which we base actions, and 4) the scientific method provides an excellent guide for such examination. The level of exposition is neither technical nor deeply philosophical
A type system is a syntactic method for enforcing levels of abstraction in programs. The study of type systems--and of programming languages from a type-theoretic perspective--has important applications in software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators.
Some of the things you can do with the GrassmannAlgebra software. You can: * Set up your own space of any dimension and metric. The default is a 3D Euclidean * Work basis-free or with a basis * Declare your own scalar symbols * Declare your own vector symbols: * Apply Grassmann operations. A Grassmann operation is any of: the complement operation and the six product operations: the exterior, regressive, interior, generalized Grassmann, hypercomplex and Clifford products. * Manipulate Grassmann expressions and numbers. A Grassmann expression is either a scalar, a Grassmann variable, or the result of a sequence of Grassmann operations or sums on Grassmann expressions. A Grassmann number is a Grassmann expression expressed as a linear combination of basis elements. * Compute the grade of any Grassmann expression. * Query the attributes of any expression. * Extract components of different types
Adam Chlipala This is the web site for an in-progress textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. This is the text for a Fall 2008 class at Harvard.
x leroy, d remy Version monolitique, Postscript, PDF; Résumé: Ce document est un cours d’introduction à la programmation du système Unix, mettant l’accent sur la communication entre les processus. La principale nouveauté de ce travail est l’utilisation du langage Objective Caml, un dialecte du langage ML, à la place du langage C qui est d’ordinaire associé à la programmation système. Ceci donne des points de vue nouveaux à la fois sur la programmation système et sur le langage ML. Introduction Généralités Les fichiers Les processus Les signaux Communications inter-processus classiques Communications modernes: les prises Les coprocessus Pour aller plus loin Références
I enjoy writing and in addition to my published books I offer free Open Content material on this web page. I both enjoy and appreciate feedback on ideas for material and reporting any errors. I offer free web books on Java and artificial intelligence programming, Common Lisp programming, and a new but still incomplete book The Software Design and Development Book. I am also working on a Ruby AI book and a short paper on AI design patterns. I also have a link to an old paper on AI, Go and Consciousness (updated 1/25/2004) available here. I have a short paper Jumpstarting the Semantic Web available here (new version 1/14/2005). I am also starting to include my fiction (short stories) here in addition to computer science web books.
The Little Book of Semaphores is a free (in both senses of the word) textbook that introduces the principles of synchronization for concurrent programming. In most computer science curricula, synchronization is a module in an Operating Systems class. OS textbooks present a standard set of problems with a standard set of solutions, but most students don't get a good understanding of the material or the ability to solve similar problems. The approach of this book is to identify patterns that are useful for a variety of synchronization problems and then show how they can be assembled into solutions. After each problem, the book offers a hint before showing a solution, giving students a better chance of discovering solutions on their own. The book covers the classical problems, including "Readers-writers," "Producer-consumer", and "Dining Philosophers." In addition, it collects a number of not-so-classical problems
Coq'Art is the familiar name for the first book on the Coq proof assistant and its underlying theory the Calculus of Inductive Constructions , written by Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Castéran, Pierre 2004, XXV, 469 p., Hardcover ISBN: 3-540-20854-2 This site has been updated for Coq8.2. Warning! Some solutions we propose don't work on versions prior to V8.2gamma. Please find here a tar file fully compatible with coq8.1pl3 and the printed edition of the book. These exercises were written after the release of the book (May 2004). The solution of some of them (e.g. mergesort ) illustrates new features of Coq. For instance, command Function and tactic functional induction.
Let Over Lambda (ISBN 978-1-4357-1275-1, 376+iv pp.) is one of the most hardcore computer programming books out there. Starting with the fundamentals, it describes the most advanced features of the most advanced language: COMMON LISP. The point of this book is to expose you to ideas that you might otherwise never be exposed to. This book is about macros, that is programs that write programs. Macros are what make lisp the greatest programming language in the world. When used properly, macros enable amazing feats of abstraction, programmer productivity, and code efficiency and security that are unheard of elsewhere. Macros let you do things you simply cannot do in other languages.