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

Tyranny from Ancient Greece to Renaissance France

This Palgrave Pivot examines how prominent thinkers throughout history, from ancient Greece to sixteenth-century France, have perceived tyrants and tyranny. Ancient philosophers such as Plato and Aristotle were the first to build a vocabulary for tyrants and the forms of government they corrupted. Thirteenth century analyses of tyranny by Thomas Aquinas and John of Salisbury, revived from Antiquity, were recast as short observations about what tyrants do. They claimed that tyrants govern for their own advantage, not for the people. Tyrants could be usurpers, increase taxes, and live in luxury. The list of tyrannical actions grew over time, especially in periods of turmoil and civil war, often raising the question: When can a tyrant be legitimately deposed or killed? In offering a brief biography of these political philosophers, including Machiavelli, Erasmus, More, Bodin, and others, along with their views on tyrannical behavior, Orest Ranum reveals how the concept of tyranny has been shaped over time, and how it still persists in political thought to this day.

A Typology of Reference Systems

This volume offers a typology of reference systems across a range of typologically and genetically distinct languages, including English, Mandarin, non-literary varieties of Russian, Chadic languages, and a number of understudied Sino-Russian idiolects. The term 'reference system' designates all functions within the grammatical system of a given language that indicate whether and how the addressee(s) should identify the referents of participants in the proposition. In this book, Zygmunt Frajzyngier explores the major functional domains, subdomains, and individual functions that determine the identification of participants in a given language, and outlines which are the most and least frequently found crosslinguistically. The findings reveal that bare nouns, pronouns, demonstratives and determiners, and coding on the verb ('agreement') have different functions in different languages. The concluding chapters offer explanations for these differences and explore their implications for the theory and methodology of syntactic analysis, for linguistic typology, and for syntactic theories.

Typicality Reasoning in Probability, Physics, and Metaphysics (New Directions in the Philosophy of Science)

This book provides a comprehensive investigation into the concept of typicality and its significance for physics and the philosophy of science. It identifies typicality as a fundamental way of reasoning, central to how natural laws explain and are tested against phenomena. The book discusses various applications of typicality to foundational questions in physics and beyond.These include:a unified interpretation of objective probabilities in classical mechanics and quantum mechanicsa detailed discussion of Boltzmann's statistical mechanics, entropy, and the second law of thermodynamicsa novel account of the asymmetry of causation and the arrow of time Finally, the book turns to the question: "What are laws of nature"? It argues that typicality extends to a powerful way of reasoning in metaphysics that can and should inform our commitments about the fundamental ontology of the world. On this basis, it develops an argument against the Humean best system account, according to which laws of nature are merely an efficient summary of contingent regularities.

Types, Tableaus, and Gödel’s God (Trends in Logic #12)

Gödel's modal ontological argument is the centerpiece of an extensive examination of intensional logic. First, classical type theory is presented semantically, tableau rules for it are introduced, and the Prawitz/Takahashi completeness proof is given. Then modal machinery is added to produce a modified version of Montague/Gallin intensional logic. Finally, various ontological proofs for the existence of God are discussed informally, and the Gödel argument is fully formalized. Parts of the book are mathematical, parts philosophical.

Types in Compilation: Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000. Revised Selected Papers (Lecture Notes in Computer Science #2071)

The importance of typed languages for building robust software systems is, by now, an undisputed fact. Years of research have led to languages with richly expressive, yet easy to use, type systems for high-level programming languages. Types provide not only a conceptual framework for language designers, but also a ord positive bene ts to the programmer, principally the ability to express and enforce levels of abstraction within a program. Early compilers for typed languages followed closely the methods used for their untyped counterparts. The role of types was limited to the earliest s- ges of compilation, and they were thereafter ignored during the remainder of the translation process. More recently, however, implementors have come to - cognize the importance of types during compilation and even for object code. Several advantages of types in compilation have been noted to date: { They support self-checking by the compiler. By tracking types during c- pilation it is possible for an internal type checker to detect translation errors at an early stage, greatly facilitating compiler development. { They support certi cation of object code. By extending types to the ge- rated object code, it becomes possible for a code user to ensure the basic integrity of that code by checking its type consistency before execution. { They support optimized data representations and calling conventions, even in the presence of modularity. By passing types at compile-, link-, and even run-time, it is possible to avoid compromises of data representation imposed by untyped compilation techniques.

Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (Lecture Notes in Computer Science #4502)

The refereed post-proceedings of the International Workshop of the Types Working Group are presented in this volume. The 17 papers address all current issues in formal reasoning and computer programming based on type theory, including languages and computerized tools for reasoning; applications in several domains, such as analysis of programming languages; certified software; formalization of mathematics; and mathematics education.

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.