Constructivity in computer science : summer symposium, San Antonio, TX, June 19-22, 1991 : proceeding
Mathematicians have long recognized the distinction between an argument showing that an interesting object exists and a procedure for actually constructing the object. Computer science adds a new dimension of interest in constructivity, since a computer program is a formal description of a construct...
Enregistré dans:
| Autres auteurs: | , |
|---|---|
| Format: | Livre numérique |
| Langue: | Anglais |
| Publié: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Collection: | Lecture notes in computer science
613 |
| Sujets: | |
| Accès en ligne: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Actes d'un symposium tenu à San Antonio du 19 au 22 juin 1991, d'après l écran-titre Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Constructivity in computer science, summer symposium, San Antonio, TX, June 19-22, 1991, proceedings, J.P. Myers, Jr., M.J. O'Donnell, eds, Berlin, Springer-Verlag, 1992, 1 vol. (X-246 p.), Lecture notes in computer science, 3-540-55631-1 • Constructivity in Computer Science, Texte imprimé, 9783662197899 |
Table des matières:
- Connecting formal semantics to constructive intuitions
- Kripke semantics for dependent type theory and realizability interpretations
- Reflective semantics of constructive type theory
- Are subsets necessary in Martin-Löf type theory?
- Development transformation based on higher order type theory
- Classical proofs as programs: How, what and why
- Classical type theory
- Axiomatization of calculus of constructions
- A logical view of assignments
- Constructivity issues in graph algorithms
- Constructive topology and combinatorics
- Implementing constructive real analysis (preliminary report)
- Examples of semicomputable sets of real and complex numbers
- Bringing mathematics education into the algorithmic age
- The type structure of CAT
- A simple and powerful approach for studying constructivity, computability, and complexity.