default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDTYPES 2003: Torino, Italy
- Stefano Berardi, Mario Coppo, Ferruccio Damiani
:
Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Lecture Notes in Computer Science 3085, Springer 2004, ISBN 3-540-22164-6 - Robin Adams:
A Modular Hierarchy of Logical Frameworks. 1-16 - Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini:
Tailoring Filter Models. 17-33 - Clemens Ballarin:
Locales and Locale Expressions in Isabelle/Isar. 34-50 - Sylvain Baro:
Introduction to PAF!, a Proof Assistant for ML Programs Verification. 51-65 - Stefan Berghofer:
A Constructive Proof of Higman's Lemma in Isabelle. 66-82 - Lorenzo Bettini, Viviana Bono, Silvia Likavec:
A Core Calculus of Higher-Order Mixins and Classes. 83-98 - Viviana Bono, Jerzy Tiuryn, Pawel Urzyczyn:
Type Inference for Nested Self Types. 99-114 - Edwin C. Brady, Conor McBride, James McKinna:
Inductive Families Need Not Store Their Indices. 115-129 - Jacek Chrzaszcz:
Modules in Coq Are and Will Be Correct. 130-146 - Horatiu Cirstea, Luigi Liquori, Benjamin Wack:
Rewriting Calculus with Fixpoints: Untyped and First-Order Systems. 147-161 - Pierre Corbineau:
First-Order Reasoning in the Calculus of Inductive Constructions. 162-177 - Ugo Dal Lago, Simone Martini, Luca Roversi:
Higher-Order Linear Ramified Recurrence. 178-193 - José Espírito Santo, Luís Pinto:
Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus. 194-209 - Nicola Gambino, Martin Hyland:
Wellfounded Trees and Dependent Polynomial Functors. 210-225 - Silvia Ghilezan, Pierre Lescanne:
Classical Proofs, Typed Processes, and Intersection Types: Extended Abstract. 226-241 - Furio Honsell, Marina Lenisa:
"Wave-Style" Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models. 242-258 - Robert Kießling, Zhaohui Luo:
Coercions in Hindley-Milner Systems. 259-275 - Yong Luo, Zhaohui Luo:
Combining Incoherent Coercions for Sigma-Types. 276-292 - Alberto Momigliano, Alwen Fernanto Tiu:
Induction and Co-induction in Sequent Calculus. 293-308 - Milad Niqui, Yves Bertot:
QArith: Coq Formalisation of Lazy Rational Arithmetic. 309-323 - Furio Honsell, Ivan Scagnetto:
Mobility Types in Coq. 324-337 - Sergei Soloviev, David Chemouil:
Some Algebraic Structures in Lambda-Calculus with Inductive Types. 338-354 - Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker:
A Concurrent Logical Framework: The Propositional Fragment. 355-377 - Freek Wiedijk:
Formal Proof Sketches. 378-393 - Hongwei Xi:
Applied Type System: Extended Abstract. 394-408
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.
last updated on 2026-07-29 23:08 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated, funded, and maintained by:
Schloss Dagstuhl - Leibniz Center for Informatics is a member of the Leibniz Association and is funded by the federal government of Germany and the states of Germany, especially Saarland and Rhineland‑Palatinate.
