top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
[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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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-9910822195503321
Sørensen Morten Heine  
Amsterdam ; ; Boston [MA], : Elsevier, 2006
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui