1.

Record Nr.

UNINA9910459824103321

Autore

Scott Cord A.

Titolo

Comics and conflict : patriotism and propaganda from WWII through Operation Iraqi Freedom / / Cord A. Scott

Pubbl/distr/stampa

Annapolis, Maryland : , : Naval Institute Press, , [2014]

©2014

ISBN

1-61251-478-2

Descrizione fisica

1 online resource (432 p.)

Classificazione

HIS027100HIS054000HIS027000

Disciplina

940.53/1

Soggetti

World War, 1939-1945 - Social aspects - United States

Comic books, strips, etc - United States - History - 20th century

Comic books, strips, etc - United States - History - 21st century

Superheroes - United States - History - 20th century

Superheroes - United States - History - 21st century

Propaganda - United States - History - 20th century

Propaganda - United States - History - 21st century

War and society - United States - History - 20th century

War and society - United States - History - 21st century

Electronic books.

Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Monografia

Note generali

Description based upon print version of record.

Nota di bibliografia

Includes bibliographical references and index.

Nota di contenuto

Cover; Title Page; Copyright; Dedication; Contents; Preface; 1. Entertaining and Informing the Masses; 2. Fighting for Freedom (1939-45); 3. The Cold War Erupts, and Comics-Mostly-Toe the Line (1945-62); 4. War Comics in a Time of Upheaval (1962-91); 5. The Resurgence of Superheroes after the Fall of Communism (1991-2001); 6. The Role of Comics after 9/11 (2001-3); 7. Comics and the Soul of Combat (2003-10); 8. Conclusion: Concepts of War through Comic Books; Appendix: The Comics Code; Notes; Bibliography; Index; The Author

Sommario/riassunto

"The comic book, which emerged in its modern form in the 1930s, was initially a form of simple, visual entertainment that gave readers, especially children, a form of escape from daily life. However, as World War II began, comic books evolved into a form of propaganda,



providing information and education for both children and adults. Comics and Conflict examines how comic books were used to display patriotism, valor and adventure through war stories, and eventually to tell of the horrors of combat from World War II through the current conflicts in Iraq and Afghanistan"--

2.

Record Nr.

UNISA996206653803316

Titolo

Chinese journal of geophysics = : Acta geophysica sinica = Di qiu wu li xue bao

Pubbl/distr/stampa

New York, : Allerton Press

Washington, DC, : American Geophysical Union

ISSN

2326-0440

Disciplina

550/.5

Soggetti

Geophysics

Periodicals.

Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Periodico

Note generali

Refereed/Peer-reviewed



3.

Record Nr.

UNINA9910784595103321

Autore

Sørensen Morten Heine

Titolo

Lectures on the Curry-Howard isomorphism [[electronic resource] /] / Morten Heine Sørensen, Paweł Urzyczyn

Pubbl/distr/stampa

Amsterdam ; ; Boston [MA], : Elsevier, 2006

ISBN

1-281-05105-5

9786611051051

0-08-047892-1

Edizione

[1st ed.]

Descrizione fisica

1 online resource (457 p.)

Collana

Studies in logic and the foundations of mathematics, , 0049-237X ; ; v. 149

Altri autori (Persone)

UrzyczynPaweł

Disciplina

511.3/26

Soggetti

Curry-Howard isomorphism

Lambda calculus

Proof theory

Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Monografia

Note generali

Description based upon print version of record.

Nota di bibliografia

Includes bibliographical references (p. 403-430) and index.

Nota di contenuto

Cover; Title Page; Copyright Page; Table of Contents; Chapter 1  Type-free Lambda-calculus; 1.1 A gentle introduction; 1.2 Pre-terms and Lambda-terms; 1.3 Reduction; 1.4 The Church-Rosser theorem; 1.5 Leftmost reductions are normalizing; 1.6 Perpetual reductions and the conservation theorem; 1.7 Expressibility and undeeidability; 1.8 Notes; 1.9 Exercises; Chapter 2  Intultionistic logic; 2.1 The BHK interpretation; 2.2 Natural deduction; 2.3 Algebraic semantics of classical logic; 2.4 Heyting algebras; 2.5 Kripke semantics; 2.6 The implicational fragment; 2.7 Notes; 2.8 Exercises

Chapter 3  Simply typed Lambda-calcuIus3.1 Simply typed Lambda-ealculus a la Curry; 3.2 Type reconstruction algorithm; 3.3 Simply typed Lambda-calculus a la Church; 3.4 Church versus Curry typing; 3.5 Normalization; 3.6 Church-Rosser property; 3.7 Expressibility; 3.8 Notes; 3.9 Exercises; Chapter 4  The Curry-Howard isomorphism; 4.1 Proofs and terms; 4.2 Type inhabitation; 4.3 Not an exact isomorphism; 4.4 Proof normalization; 4.5 Sums and products; 4.6 Prover-skeptic dialogues; 4.7 Prover-skeptic dialogues with absurdity; 4.8 Notes; 4.9 Exercises; Chapter 5  Proofs as combinators



5.1 Hubert style proofs5.2 Combinatory logic; 5.3 Typed combinators; 5.4 Combinators versus lambda terms; 5.5 Extensionality; 5.6 Relevance and linearity; 5.7 Notes; 5.8 Exercises; Chapter 6  Classical logic and control operators; 6.1 Classical prepositional lope; 6.2 The Lambda meu-calculus; 6.3 Subject reduction, confluence, strong normalization; 6.4 Logical embedding and CPS translation; 6.5 Classical prover-skeptic dialogues; 6.6 The pure implicational fragment; 6.7 Conjunction and disjunction; 6.8 Notes; 6.9 Exercises; Chapter 7  Sequent calculus; 7.1 Gentzen's sequent calculus LK

7.2 Fragments of LK versus natural deduction7.3 Gentzen's Hauptaatz; 7.4 Cut elimination versus normalization; 7.5 Lorenzen dialogues; 7.6 Notes; 7.7 Exercises; Chapter 8  First-order logic; 8.1 Syntax of first-order logic; 8.2 Informal semantics; 8.3 Proof systems; 8.4 Classical semantics; 8.5 Algebraic semantics of intuitionistie logic; 8.6 Kripke semantics; 8.7 Lambda-calculus; 8.8 Undeddability; 8.9 Notes; 8.10 Exercises; Chapter 9  First-order arithmetic; 9.1 The language of arithmetic; 9.2 Peano Arithmetic; 9.3 Godel's theorems; 9.4 Representable and provably recursive functions

9.5 Heyting Arithmetic9.6 Kleene's realfeability interpretation; 9.7 Notes; 9.8 Exercises; Chapter 10  Godel's system T; 10.1 From Heyting Arithmetic to system T; 10.2 Syntax; 10.3 Strong normalization; 10.4 Modified realizability; 10.5 Notes; 10.6 Exercises; Chapter 11  Second-order logic and polymorphism; 11.1 Prepositional second-order logic; 11.2 Polymorphic lambda-calculus (system F); 11.3 Expressive power; 11.4 Gurry-style polymorphism; 11.5 Strong normalization; 11.6 The inhabitation problem; 11.7 Higher-order polymorphism; 11.8 Notes; 11.9 Exercises

Chapter 12  Second-order arithmetic

Sommario/riassunto

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.The isomorphism has many aspects, even at the syntactic level:formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation,