1.

Record Nr.

UNISA996465637503316

Titolo

Mathematics of Program Construction [[electronic resource] ] : 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010, Proceedings / / edited by Claude Bolduc, Jules Desharnais, Bechir Ktari

Pubbl/distr/stampa

Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010

ISBN

1-280-38680-0

9786613564726

3-642-13321-5

Edizione

[1st ed. 2010.]

Descrizione fisica

1 online resource (X, 427 p. 57 illus.)

Collana

Theoretical Computer Science and General Issues, , 2512-2029 ; ; 6120

Disciplina

005.10151

Soggetti

Software engineering

Immunology

Computer programming

Computer science

Machine theory

Software Engineering

Programming Techniques

Computer Science Logic and Foundations of Programming

Formal Languages and Automata Theory

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 and index.

Nota di contenuto

Invited Talks -- The Algorithmics of Solitaire-Like Games -- Compositionality of Secure Information Flow -- Process Algebras for Collective Dynamics -- Contributed Talks -- On Automated Program Construction and Verification -- The Logic of Large Enough -- Dependently Typed Grammars -- Abstraction of Object Graphs in Program Verification -- Subtyping, Declaratively -- Compositional Action System Derivation Using Enforced Properties -- Designing an Algorithmic Proof of the Two-Squares Theorem -- Partial, Total and General Correctness -- Unifying Theories of Programming That Distinguish Nontermination and Abort -- Adjoint Folds and Unfolds --



An Abstract Machine for the Old Value Retrieval -- A Tracking Semantics for CSP -- Matrices as Arrows! -- Lucy-n: a n-Synchronous Extension of Lustre -- Sampling, Splitting and Merging in Coinductive Stream Calculus -- Generic Point-free Lenses -- Formal Derivation of Concurrent Garbage Collectors -- Temporal Logic Verification of Lock-Freedom -- Gradual Refinement.