1.

Record Nr.

UNISA990000936970203316

Titolo

Stochastic networks / Frank P. Kelly, Ruth J. Williams editors

ISBN

0-387-94531-8

Descrizione fisica

XXXI, 427 p. ; 24 cm

New York : Springer ; c1995

Collana

The IMA volumes in mathematics and its applicatrions ; 71

Disciplina

519.82

Soggetti

Teoria delle code

Collocazione

519.82 STO

Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Monografia

2.

Record Nr.

UNISA996465407003316

Titolo

Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers / / edited by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack

Pubbl/distr/stampa

Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002

ISBN

3-540-45842-5

Edizione

[1st ed. 2002.]

Descrizione fisica

1 online resource (VIII, 248 p.)

Collana

Lecture Notes in Computer Science, , 0302-9743 ; ; 2277

Disciplina

006.3/33

Soggetti

Computer logic

Architecture, Computer

Mathematical logic

Programming languages (Electronic computers)

Artificial intelligence

Logics and Meanings of Programs

Computer System Implementation

Mathematical Logic and Foundations

Mathematical Logic and Formal Languages

Programming Languages, Compilers, Interpreters

Artificial Intelligence



Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Monografia

Note generali

Bibliographic Level Mode of Issuance: Monograph

Nota di bibliografia

Includes bibliographical references at the end of each chapters and index.

Nota di contenuto

Collection Principles in Dependent Type Theory -- Executing Higher Order Logic -- A Tour with Constructive Real Numbers -- An Implementation of Type:Type -- On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem -- Constructive Reals in Coq: Axioms and Categoricity -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals -- A Kripke-Style Model for the Admissibility of Structural Rules -- Towards Limit Computable Mathematics -- Formalizing the Halting Problem in a Constructive Type Theory -- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory -- Changing Data Structures in Type Theory: A Study of Natural Numbers -- Elimination with a Motive -- Generalization in Type Theory Based Proof Assistants -- An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma.