Browse Results

Select your format based upon: 1) how you want to read your book, and 2) compatibility with your reading tool. To learn more about using Bookshare with your device, visit the Help Center.

Here is an overview of the specialized formats that Bookshare offers its members with links that go to the Help Center for more information.

• Bookshare Web Reader - A customized reading tool for Bookshare members offering all the features of DAISY with a single click of the "Read Now" link.
• DAISY (Digital Accessible Information System) - A digital book file format. DAISY books from Bookshare are DAISY 3.0 text files that work with just about every type of access technology that reads text. Books that contain images will have the download option of ‘DAISY Text with Images’.
• BRF (Braille Refreshable Format) - Digital Braille for use with refreshable Braille devices and Braille embossers.
• MP3 (MPEG audio layer 3) - Provides audio only with no text. These books are created with a text-to-speech engine and spoken by Kendra, a high quality synthetic voice from Ivona. Any device that supports MP3 playback is compatible.
• DAISY Audio - Similar to the DAISY option above; however, this option uses MP3 files created with our text-to-speech engine that utilizes Ivonas Kendra voice. This format will work with Daisy Audio compatible players such as Victor Reader Stream and Read2Go.
• EPUB - A standard e-book format that can be read on many tools, such as iBooks, Readium or others.
• Word - Accessible Word output, which can be unzipped and opened in any tool that allows .docx files

Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers (Lecture Notes in Computer Science #1657)

Types for Proofs and Programs: International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers (Lecture Notes in Computer Science #3085)

These proceedings contain a selection of refereed papers presented at or related to the 3rd Annual Workshop of the Types Working Group (Computer-Assisted Reasoning Based on Type Theory, EU IST project 29001), which was held d- ing April 30 to May 4, 2003, in Villa Gualino, Turin, Italy. The workshop was attended by about 100 researchers. Out of 37 submitted papers, 25 were selected after a refereeing process. The ?nal choices were made by the editors. Two previous workshops of the Types Working Group under EU IST project 29001 were held in 2000 in Durham, UK, and in 2002 in Berg en Dal (close to Nijmegen), The Netherlands. These workshops followed a series of meetings organized in the period 1993–2002 within previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these e- lier workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 2277, and 2646. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: Design, Implementation and Ex- riments. Proceedings for annual meetings under that action were published by Cambridge University Press in the books “Logical Frameworks”, and “Logical Environments”, edited by G. Huet and G. Plotkin. We are very grateful to the members of the research group “Semantics and Logics of Computation” of the Computer Science Department of the University of Turin, who helped organize the Types 2003 meeting in Torino.

Types for Proofs and Programs: International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers (Lecture Notes in Computer Science #5497)

These proceedings contain a selection of refereed papers presented at or - lated to the Annual Workshop of the TYPES project (EU coordination action 510996), which was held during March 26–29, 2008 in Turin, Italy. The topic of this workshop, and of all previous workshops of the same project, was f- mal reasoning and computer programming based on type theory: languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certi?ed software, mobile code, formali- tion of mathematics, mathematics education. The workshop was attended by more than 100 researchers and included more than 40 presentations. We also had three invited lectures, from A. Asperti (University of Bologna), G. Dowek (LIX, Ecole polytechnique, France) and J. W. Klop (Vrije Universiteit, A- terdam, The Netherlands). From 27 submitted papers, 19 were selected after a reviewing process. Each submitted paper was reviewed by three referees; the ?nal decisions were made by the editors. This workshop is the last of a series of meetings of the TYPES working group funded by the European Union (IST project 29001, ESPRIT Working Group 21900, ESPRIT BRA 6435).

Types for Proofs and Programs: International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers (Lecture Notes in Computer Science #2277)

Types for Proofs and Programs: International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers (Lecture Notes in Computer Science #1956)

Types for Proofs and Programs: International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers (Lecture Notes in Computer Science #3839)

The 17 revised full papers presented here cover all current issues of formal reasoning and computer programming based on type theory are addressed; in particular languages and computerised tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education.

Types for Proofs and Programs: Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers (Lecture Notes in Computer Science #2646)

These proceedings contain a refereed selection of papers presented at the Second Annual Workshop of the Types Working Group (Computer-Assisted Reasoning based on Type Theory, EUIST project 29001), which was held April 24–28, 2002 in Hotel Erica, Berg en Dal (close to Nijmegen), The Netherlands. The workshop was attended by about 90 researchers. On April 27, there was a special afternoon celebrating the 60th birthday of Per Martin-L¨of, one of the founding fathers of the Types community. The afternoon consisted of the following three invited talks: “Constructive Validity Revisited” by Dana Scott, “From the Rules of Logic to the Logic of Rules” by Jean-Yves Girard, and “The Varieties of Type Theories” by Peter Aczel. The contents of these contributions were not laid down in these proceedings, but the videos of the talks and the slides used by the speakers are available at http://www. cs. kun. nl/fnds/MartinLoefDay/LoefTalks. htm The previous workshop of the Types Working Group under EUIST project 29001 was held in 2000 in Durham, UK. The workshops Types 2000 and Types 2002 followed a series of meetings organized in the period 1993 – 1999 whithin previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these earlier Types workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 1956 and 2277. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: - sign, Implementation and Experiments.

Types for Proofs and Programs: International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers (Lecture Notes in Computer Science #4941)

This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2007, the concluding conference of the Types project, held in Cividale del Friuli, Italy, in May 2007. The 13 revised full papers presented were carefully reviewed and selected from 22 submissions. The topic of this last annual workshop of the Types Working Group was formal reasoning and computer programming based on type theory. Great importance was attached to languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalization of mathematics and mathematics education.

Typen moderner Demokratietheorien: Überblick und Sortierungsvorschlag (essentials)

Das essential bietet einen kompakten Überblick über die neuere Entwicklung der Demokratietheorie und nimmt eine prägnante Sortierung der gegenwärtigen Theorien in diesem Bereich vor. Hubertus Buchstein erläutert die methodischen Unterschiede zwischen den konkurrierenden demokratietheoretischen Ansätzen und stellt vier grundlegende Typen moderner Demokratietheorien vor: historische, empirische, formale und normative Demokratietheorien. Viele Debatten in der Öffentlichkeit, der Politischen Bildung und der Politikwissenschaft über die Demokratie lassen sich mit mehr Gewinn führen, wenn man die unterschiedlichen Blickwinkel der vier Typen beachtet. Dieses essential liefert einen wichtigen Beitrag dazu.

Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001 Krakow, Poland, May 2-5, 2001 Proceedings (Lecture Notes in Computer Science #2044)

This book constitutes the refereed proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, TLCA 2001, held in Krakow, Poland in May 2001. The 28 revised full papers presented were carefully reviewed and selected from 55 submissions. The volume reports research results on all current aspects of typed lambda calculi. Among the topics addressed are type systems, subtypes, coalgebraic methods, pi-calculus, recursive games, various types of lambda calculi, reductions, substitutions, normalization, linear logic, cut-elimination, prelogical relations, and mu calculus.

Typed Lambda Calculi and Applications: 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009, Proceedings (Lecture Notes in Computer Science #5608)

This book constitutes the refereed proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19th International Conference on Rewriting Techniques and Applications as part of RDP 2009, the 5th International Conference on Rewriting, Deduction, and Programming. The 27 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 53 submissions. The papers present original research results that are broadly relevant to the theory and applications of typed calculi and address a wide variety of topics such as proof-theory, semantics, implementation, types, and programming.

Typed Lambda Calculi and Applications: 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings (Lecture Notes in Computer Science #1581)

Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013, Proceedings (Lecture Notes in Computer Science #7941)

This book constitutes the refereed proceedings of the 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, held in Eindhoven, The Netherlands, in June 2013 as part of RDP 2013, the 7th Federated Conference on Rewriting, Deduction, and Programming, together with the 24th International Conference on Rewriting Techniques and Applications, RTA 2013, and several related events. The 15 revised full papers presented were carefully reviewed and selected from 41 submissions. The papers provide prevailing research results on all current aspects of typed lambda calculi, ranging from theoretical and methodological issues to applications in various contexts addressing a wide variety of topics such as proof-theory, semantics, implementation, types, and programming.

Typed Lambda Calculi and Applications: 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings (Lecture Notes in Computer Science #2701)

The refereed proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, TLCA 2003, held in Valencia, Spain in June 2003. The 21 revised full papers presented were carefully reviewed and selected from 40 submissions. The volume reports research results on all current aspects of typed lambda calculi, ranging from theoretical and methodological issues to the application of proof assistants.

Typed Lambda Calculi and Applications: 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings (Lecture Notes in Computer Science #6690)

This book constitutes the refereed proceedings of the 10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, held in Novi Sad, Serbia, in June 2011 as part of RDP 2011, the 6th Federated Conference on Rewriting, Deduction, and Programming. The 15 revised full papers presented were carefully reviewed and selected from 44 submissions. The papers provide prevailing research results on all current aspects of typed lambda calculi, ranging from theoretical and methodological issues to applications in various contexts addressing a wide variety of topics such as proof-theory, semantics, implementation, types, and programming.

Typed Lambda Calculi and Applications: 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings (Lecture Notes in Computer Science #4583)

Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings (Lecture Notes in Computer Science #3461)

The 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005) was held in Nara (Japan) from 21 to 23 April 2005, as part of the Joint Conference on Rewriting, Deduction and Programming (RDP 2005). This book contains the contributed papers, and extended abstracts of two invited talks, given by Thierry Coquand and Susumu Hayashi. A short abstract of the joint RDP invited lecture by Amy Felty is also included. The 27 contributed papers were selected from 61 submissions of generally very high quality, and the Program Committee had a hard time making the selection. The editor would like to thank everyone who submitted a paper and to express his regret that many interesting works could not be included. The editor also wishes to thank the invited speakers, the members of the Program and Organizing Committees, the Publicity Chair, and the referees for their joint e?ort towards the success of the conference. The support from the Nara Convention Bureau is gratefully acknowledged. The typed lambda calculus continues to be an important tool in logic and theoretical computer science. Since 1993, the research progress in this area has been documented by the TLCA proceedings. The present volume contributes to this tradition.

The Type Theory of Law: An Essay in Psychoanalytic Jurisprudence (SpringerBriefs in Law)

This volume presents a Type Theory of Law (TTL), claiming that this is a unique theory of law that stems from the philosophical understanding of Jung’s psychological types applied to the phenomenon of law. Furthermore, the TTL claims to be a universal, general and descriptive account of law. To prove that, the book first presents the fundamentals of Jungian psychological types, as they had been invented by Jung and consequently developed further by his followers. The next part of the book describes how the typological structure of an individual determines their understanding of law. It then addresses the way in which inclusive legal theory can be understood based on this typology. Finally, the book describes the TTL in general and descriptive terms and puts it into context. All in all, the book shows how the integral or inclusive approach to understanding the nature of law is not only in tune with our time, but also relevant for presenting a more persuasive picture of law than the older exclusivist or dualist approaches of strict natural law and rigid legal positivism did.

Type Systems for Distributed Programs: Components and Sessions (Atlantis Studies in Computing #7)

In this book we develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems are an adequate methodology considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like deadlock or lock freedom in concurrent settings.The main contributions of this book are twofold.i) We design a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations.ii) We define an encoding of the session pi-calculus, which models communication in distributed systems, into the standard typed pi-calculus. We use this encoding to derive properties like type safety and progress in the session pi-calculus by exploiting the corresponding properties in the standard typed pi-calculus.

Type Logical Grammar: Categorial Logic of Signs

Type-2 Fuzzy Logic: Theory and Applications (Studies in Fuzziness and Soft Computing #223)

This book describes new methods for building intelligent systems using type-2 fuzzy logic and soft computing (SC) techniques. The authors extend the use of fuzzy logic to a higher order, which is called type-2 fuzzy logic. Combining type-2 fuzzy logic with traditional SC techniques, we can build powerful hybrid intelligent systems that can use the advantages that each technique offers. This book is intended to be a major reference tool and can be used as a textbook.

Tychomancy: Inferring Probability From Causal Structure

Michael Strevens makes three claims about rules for inferring physical probability. They are reliable. They constitute a key part of the physical intuition that allows us to navigate the world safely in the absence of scientific knowledge. And they played a crucial role in scientific innovation, from statistical physics to natural selection.

Tychomancy: Inferring Probability From Causal Structure

Michael Strevens makes three claims about rules for inferring physical probability. They are reliable. They constitute a key part of the physical intuition that allows us to navigate the world safely in the absence of scientific knowledge. And they played a crucial role in scientific innovation, from statistical physics to natural selection.

Two Views of Virtue: Absolute Relativism and Relative Absolutism (Contributions in Philosophy)

Centore's work is an inquiry into the weaknesses and strengths of the two basic positions in ethics: the man-centered model and the God-centered model for deciding between right and wrong behavior. The philosophical paradigm for the man-centered approach is absolute relativism, while the paradigm for the God-centered approach is relative absolutism. Centore argues that the man-centered model in actual practice proves not to be realistic as an ethical guide, while the God-centered model, if properly understood, is the most useful approach. This work penetrates difficult ethical issues by examining human experience and reasoning in conjunction with actual choices of action. Although the God-centered approach is shown to be the most practical, Centore argues for a natural moral law that avoids any specific theology.Each chapter discusses the historical and theoretical background of the approaches and two possible compromises. The work is enlivened with examples of possible contexts in which moral decisions must take place. Various ethical dilemmas are presented with an examination of the potential consequences of applying either the atheistic or the theistic ethical approach. Centore's argument is complex, but he explains the elements clearly and his conclusion is strengthened by real-life cases and an extensive Bibliography.

The Two-Valued Iterative Systems of Mathematical Logic. (AM-5), Volume 5

The description for this book, The Two-Valued Iterative Systems of Mathematical Logic. (AM-5), Volume 5, will be forthcoming.