Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
The lambda calculus : its syntax and semantics / H. P. Barendregt
| The lambda calculus : its syntax and semantics / H. P. Barendregt |
| Autore | Barendregt, Hendrik Peter |
| Pubbl/distr/stampa | Amsterdam : North-Holland, 1981 |
| Descrizione fisica | xiv, 615 p. : ill. ; 23 cm. |
| Disciplina | 511.3 |
| Collana | Studies in logic and the foundations of mathematics, ISSN 0049237X ; 103 |
| Soggetto topico |
Combinatory logic and lambda-calculus
Lambda calculus |
| ISBN | 0444854908 |
| Classificazione | AMS 03B40 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISALENTO-991001056639707536 |
Barendregt, Hendrik Peter
|
||
| Amsterdam : North-Holland, 1981 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. del Salento | ||
| ||
Lambda calculus with types / / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions from Fabio Alessi [and others] [[electronic resource]]
| Lambda calculus with types / / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions from Fabio Alessi [and others] [[electronic resource]] |
| Autore | Barendregt H. P (Hendrik Pieter) |
| Pubbl/distr/stampa | Cambridge : , : Cambridge University Press, , 2013 |
| Descrizione fisica | 1 online resource (xxii, 833 pages) : digital, PDF file(s) |
| Disciplina | 511.35 |
| Collana | Perspectives in logic |
| Soggetto topico | Lambda calculus |
| ISBN |
1-139-89197-9
1-107-27172-X 1-107-27381-1 1-107-27504-0 1-107-27707-8 1-139-03263-1 1-107-27830-9 1-299-77274-9 1-107-47131-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction -- Part 1. Simple types. The simply typed lambda calculus -- Properties -- Tools -- Definability, unification and matching -- Extensions -- Applications -- Part II. Recursive types. The systems -- Properties of recursive types -- Properties of terms with types -- Models -- Applications -- Part III. Intersection types. An example system -- Type assignment systems -- Basic properties of intersection type assignment -- Type and lambda structures -- Filter models -- Advanced properties and applications. |
| Record Nr. | UNINA-9910464948403321 |
|
Barendregt H. P (Hendrik Pieter)
|
||
| Cambridge : , : Cambridge University Press, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Lambda calculus with types / / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions from Fabio Alessi [and others] [[electronic resource]]
| Lambda calculus with types / / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions from Fabio Alessi [and others] [[electronic resource]] |
| Autore | Barendregt H. P (Hendrik Pieter) |
| Pubbl/distr/stampa | Cambridge : , : Cambridge University Press, , 2013 |
| Descrizione fisica | 1 online resource (xxii, 833 pages) : digital, PDF file(s) |
| Disciplina | 511.35 |
| Collana | Perspectives in logic |
| Soggetto topico | Lambda calculus |
| ISBN |
1-139-89197-9
1-107-27172-X 1-107-27381-1 1-107-27504-0 1-107-27707-8 1-139-03263-1 1-107-27830-9 1-299-77274-9 1-107-47131-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction -- Part 1. Simple types. The simply typed lambda calculus -- Properties -- Tools -- Definability, unification and matching -- Extensions -- Applications -- Part II. Recursive types. The systems -- Properties of recursive types -- Properties of terms with types -- Models -- Applications -- Part III. Intersection types. An example system -- Type assignment systems -- Basic properties of intersection type assignment -- Type and lambda structures -- Filter models -- Advanced properties and applications. |
| Record Nr. | UNINA-9910789313503321 |
|
Barendregt H. P (Hendrik Pieter)
|
||
| Cambridge : , : Cambridge University Press, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Lambda calculus with types / / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions from Fabio Alessi [and others] [[electronic resource]]
| Lambda calculus with types / / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions from Fabio Alessi [and others] [[electronic resource]] |
| Autore | Barendregt H. P (Hendrik Pieter) |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Cambridge : , : Cambridge University Press, , 2013 |
| Descrizione fisica | 1 online resource (xxii, 833 pages) : digital, PDF file(s) |
| Disciplina | 511.35 |
| Collana | Perspectives in logic |
| Soggetto topico | Lambda calculus |
| ISBN |
1-139-89197-9
1-107-27172-X 1-107-27381-1 1-107-27504-0 1-107-27707-8 1-139-03263-1 1-107-27830-9 1-299-77274-9 1-107-47131-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction -- Part 1. Simple types. The simply typed lambda calculus -- Properties -- Tools -- Definability, unification and matching -- Extensions -- Applications -- Part II. Recursive types. The systems -- Properties of recursive types -- Properties of terms with types -- Models -- Applications -- Part III. Intersection types. An example system -- Type assignment systems -- Basic properties of intersection type assignment -- Type and lambda structures -- Filter models -- Advanced properties and applications. |
| Record Nr. | UNINA-9910822226703321 |
|
Barendregt H. P (Hendrik Pieter)
|
||
| Cambridge : , : Cambridge University Press, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
[Lambda]-calculus and computer science theory : proceedings of the symposium held in Rome, March 25-27, 1975 / IAC-CNR, Istituto per le applicazioni del calcolo "Mauro Picone" of the Consiglio nazionale delle ricerche ; edited by C. Bohm
| [Lambda]-calculus and computer science theory : proceedings of the symposium held in Rome, March 25-27, 1975 / IAC-CNR, Istituto per le applicazioni del calcolo "Mauro Picone" of the Consiglio nazionale delle ricerche ; edited by C. Bohm |
| Autore | Istituto per le applicazioni del calcolo |
| Pubbl/distr/stampa | Berlin ; New York : Springer-Verlag, 1975 |
| Descrizione fisica | xii, 370 p. : ill. ; 24 cm. |
| Disciplina | 511.3 |
| Altri autori (Persone) | Bohm, C. |
| Soggetto topico |
Combinatory logic - Congresses
Lambda calculus Programming languages - Congresses |
| ISBN | 3540074163 |
| Classificazione |
AMS 03-06
AMS 03B40 AMS 68-06 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISALENTO-991001056669707536 |
|
Istituto per le applicazioni del calcolo
|
||
| Berlin ; New York : Springer-Verlag, 1975 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. del Salento | ||
| ||
Lectures on the Curry-Howard isomorphism [[electronic resource] /] / Morten Heine Sørensen, Paweł Urzyczyn
| Lectures on the Curry-Howard isomorphism [[electronic resource] /] / Morten Heine Sørensen, Paweł Urzyczyn |
| Autore | Sørensen Morten Heine |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Amsterdam ; ; Boston [MA], : Elsevier, 2006 |
| Descrizione fisica | 1 online resource (457 p.) |
| Disciplina | 511.3/26 |
| Altri autori (Persone) | UrzyczynPaweł |
| Collana | Studies in logic and the foundations of mathematics |
| Soggetto topico |
Curry-Howard isomorphism
Lambda calculus Proof theory |
| Soggetto genere / forma | Electronic books. |
| ISBN |
1-281-05105-5
9786611051051 0-08-047892-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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 |
| Record Nr. | UNINA-9910457434803321 |
|
Sørensen Morten Heine
|
||
| Amsterdam ; ; Boston [MA], : Elsevier, 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Lectures on the Curry-Howard isomorphism [[electronic resource] /] / Morten Heine Sørensen, Paweł Urzyczyn
| Lectures on the Curry-Howard isomorphism [[electronic resource] /] / Morten Heine Sørensen, Paweł Urzyczyn |
| Autore | Sørensen Morten Heine |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Amsterdam ; ; Boston [MA], : Elsevier, 2006 |
| Descrizione fisica | 1 online resource (457 p.) |
| Disciplina | 511.3/26 |
| Altri autori (Persone) | UrzyczynPaweł |
| Collana | Studies in logic and the foundations of mathematics |
| Soggetto topico |
Curry-Howard isomorphism
Lambda calculus Proof theory |
| ISBN |
1-281-05105-5
9786611051051 0-08-047892-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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 |
| Record Nr. | UNINA-9910784595103321 |
|
Sørensen Morten Heine
|
||
| Amsterdam ; ; Boston [MA], : Elsevier, 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Lectures on the Curry-Howard isomorphism [e-book] / Morten Heine Sørensen, Paweł Urzyczyn
| Lectures on the Curry-Howard isomorphism [e-book] / Morten Heine Sørensen, Paweł Urzyczyn |
| Autore | Sørensen, Morten Heine |
| Pubbl/distr/stampa | Amsterdam ; Boston : Elsevier, 2006 |
| Descrizione fisica | xiv, 442 p. : ill. ; 24 cm |
| Disciplina | 511.326 |
| Altri autori (Persone) | Urzyczyn, Pawełauthor |
| Collana | Studies in logic and the foundations of mathematics, 0049-237X ; 149 |
| Soggetto topico |
Curry-Howard isomorphism
Lambda calculus |
| ISBN |
9780444520777
0444520775 |
| Formato | Risorse elettroniche  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISALENTO-991003277399707536 |
|
Sørensen, Morten Heine
|
||
| Amsterdam ; Boston : Elsevier, 2006 | ||
| Risorse elettroniche | ||
| Lo trovi qui: Univ. del Salento | ||
| ||
I modelli del [lambda]-calcolo e dell'aritmetica di Peano / U. Maionchi, S. Berestovoy, G. Longo
| I modelli del [lambda]-calcolo e dell'aritmetica di Peano / U. Maionchi, S. Berestovoy, G. Longo |
| Autore | Maionchi. U. |
| Pubbl/distr/stampa | [Roma] : CNR (Consiglio Nazionale delle Ricerche), 1981 |
| Descrizione fisica | 96 p. ; 25 cm. |
| Disciplina | 511.3 |
| Altri autori (Persone) |
Berestovoy, S.
Longo, Giuseppe |
| Collana | Quaderni dei Gruppi di ricerca matematica del Consiglio Nazionale delle Ricerche |
| Soggetto topico |
Combinatory logic
Lambda calculus |
| Classificazione | AMS 03B40 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | ita |
| Record Nr. | UNISALENTO-991001150359707536 |
|
Maionchi. U.
|
||
| [Roma] : CNR (Consiglio Nazionale delle Ricerche), 1981 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. del Salento | ||
| ||
Processes, terms and cycles : steps on the road to infinity : essays dedicated to Jan Willem Klop on the occasion of his 60th birthday / / Aart Middeldorp ... [et al.] (eds.)
| Processes, terms and cycles : steps on the road to infinity : essays dedicated to Jan Willem Klop on the occasion of his 60th birthday / / Aart Middeldorp ... [et al.] (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, : Springer-Verlag, c2005 |
| Descrizione fisica | 1 online resource (XVIII, 642 p.) |
| Disciplina | 005.131 |
| Altri autori (Persone) |
MiddeldorpAart <1963->
KlopJ. W |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Lambda calculus
Rewriting systems (Computer science) Machine theory |
| ISBN | 3-540-32425-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Spectra of Words -- On the Undecidability of Coherent Logic -- Löb’s Logic Meets the ?-Calculus -- A Characterisation of Weak Bisimulation Congruence -- Böhm’s Theorem, Church’s Delta, Numeral Systems, and Ershov Morphisms -- Explaining Constraint Programming -- Sharing in the Weak Lambda-Calculus -- Term Rewriting Meets Aspect-Oriented Programming -- Observing Reductions in Nominal Calculi Via a Graphical Encoding of Processes -- Primitive Rewriting -- Infinitary Rewriting: From Syntax to Semantics -- Reducing Right-Hand Sides for Termination -- Reduction Strategies for Left-Linear Term Rewriting Systems -- Higher-Order Rewriting: Framework, Confluence and Termination -- Timing the Untimed: Terminating Successfully While Being Conservative -- Confluence of Graph Transformation Revisited -- Compositional Reasoning for Probabilistic Finite-State Behaviors -- Finite Equational Bases in Process Algebra: Results and Open Questions -- Skew and ?-Skew Confluence and Abstract Böhm Semantics -- A Mobility Calculus with Local and Dependent Types -- Model Theory for Process Algebra -- Expression Reduction Systems and Extensions: An Overview -- Axiomatic Rewriting Theory I: A Diagrammatic Standardization Theorem. |
| Record Nr. | UNINA-9910483407303321 |
| Berlin, : Springer-Verlag, c2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Soggetto topico
-
Lambda calculus
(14)
- Curry-Howard isomorphism (3)
- Proof theory (2)
- Calculus (1)
- Combinatory logic (1)