![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
TYPES 2008: Torino, Italy
- Stefano Berardi, Ferruccio Damiani
, Ugo de'Liguoro:
Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers. Lecture Notes in Computer Science 5497, Springer 2009, ISBN 978-3-642-02443-6 - Davide Ancona, Giovanni Lagorio
, Elena Zucca:
Type Inference by Coinductive Logic Programming. 1-18 - Andrea Asperti
, Wilmer Ricciotti:
About the Formalization of Some Results by Chebyshev in Number Theory. 19-31 - Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini:
A New Elimination Rule for the Calculus of Inductive Constructions. 32-48 - Juan Manuel Crespo, Gustavo Betarte, Carlos Luna:
A Framework for the Analysis of Access Control Models for Interactive Mobile Devices. 49-63 - Jörg Endrullis
, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Roel C. de Vrijer:
Proving Infinitary Normalization. 64-82 - Erik Ernst:
First-Class Object Sets. 83-99 - José Espírito Santo
, Ralph Matthes, Luís Pinto
:
Monadic Translation of Intuitionistic Sequent Calculus. 100-116 - Camillo Fiorentini
, Alberto Momigliano
, Mario Ornaghi:
Towards a Type Discipline for Answer Set Programming. 117-135 - Marco Gaboardi, Simona Ronchi Della Rocca:
Type Inference for a Polynomial Lambda Calculus. 136-152 - Florian Haftmann, Makarius Wenzel:
Local Theory Specifications in Isabelle/Isar. 153-168 - Clément Houtmann:
Axiom Directed Focusing. 169-185 - Dag Hovland
:
A Type System for Usage of Software Components. 186-202 - Cezary Kaliszyk
, Freek Wiedijk:
Merging Procedural and Declarative Proof. 203-219 - Yves Bertot, Ekaterina Komendantskaya:
Using Structural Recursion for Corecursion. 220-236 - Zhaohui Luo:
Manifest Fields and Module Mechanisms in Intensional Type Theory. 237-255 - Eelis van der Weegen, James McKinna:
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. 256-271 - Milad Niqui:
Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme. 272-288 - Luca Paolini
, Mauro Piccolo:
A Process-Model for Linear Programs. 289-305 - Luca Roversi
, Luca Vercelli:
Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets. 306-322
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.