This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2008, the last of a series of meetings of the TYPES working group funded by the European Union between 1993 and 2008; the workshop has been held in Torino, Italy, in March 2008.
The 19 revised full papers presented were carefully reviewed and selected from 27 submissions. The topic of the workshop was formal reasoning and computer programming based on type theory: languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, mobile code, formalization of mathematics, mathematics education.
Author(s): Davide Ancona, Giovanni Lagorio, Elena Zucca (auth.), Stefano Berardi, Ferruccio Damiani, Ugo de’Liguoro (eds.)
Series: Lecture Notes in Computer Science 5497 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 323
City: New York
Tags: Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Programming Languages, Compilers, Interpreters; Symbolic and Algebraic Manipulation; Artificial Intelligence (incl. Robotics)
Front Matter....Pages -
Type Inference by Coinductive Logic Programming....Pages 1-18
About the Formalization of Some Results by Chebyshev in Number Theory....Pages 19-31
A New Elimination Rule for the Calculus of Inductive Constructions....Pages 32-48
A Framework for the Analysis of Access Control Models for Interactive Mobile Devices....Pages 49-63
Proving Infinitary Normalization....Pages 64-82
First-Class Object Sets....Pages 83-99
Monadic Translation of Intuitionistic Sequent Calculus....Pages 100-116
Towards a Type Discipline for Answer Set Programming....Pages 117-135
Type Inference for a Polynomial Lambda Calculus....Pages 136-152
Local Theory Specifications in Isabelle/Isar....Pages 153-168
Axiom Directed Focusing....Pages 169-185
A Type System for Usage of Software Components....Pages 186-202
Merging Procedural and Declarative Proof....Pages 203-219
Using Structural Recursion for Corecursion....Pages 220-236
Manifest Fields and Module Mechanisms in Intensional Type Theory....Pages 237-255
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq....Pages 256-271
Coalgebraic Reasoning in Coq: Bisimulation and the λ -Coiteration Scheme....Pages 272-288
A Process-Model for Linear Programs....Pages 289-305
Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets....Pages 306-322
Back Matter....Pages -
