Types for proofs and programs : international workshop, TYPES 2002, Berg en Dal, the Netherlands, April 24-28, 2002 : selected papers

Types for proofs and programs : international workshop, TYPES 2002, Berg en Dal, the Netherlands, April 24-28, 2002 : selected papers

These proceedings contain a refereed selection of papers presented at the Second Annual Workshop of the Types Working Group (Computer-Assisted Reasoning based on Type Theory, EUIST project 29001), which was held April 24 28, 2002 in Hotel Erica, Berg en Dal (close to Nijmegen), The Netherlands. The...

Descripció completa

Guardat en:
Dades bibliogràfiques
Autor corporatiu: TYPES 2002 :Berg en Dal, NL
Altres autors: Geuvers, Herman (Director editorial), Wiedijk, Freek (Director editorial)
Format: Livre numérique
Idioma:Anglais
Publicat: Berlin [etc.] : Springer [20..].
Cham : Springer Nature
Col·lecció:Lecture notes in computer science 2646
Matèries:
Informatique
Langages de programmation
Ordinateurs
Intelligence artificielle
Logique symbolique et mathématique
Théorèmes > Démonstration automatique
Actes de congrès
Accés en línia:Accès sur la plateforme de l'éditeur
Accès sur la plateforme Istex
Accès Université d'Orléans
Accès INSA CVL
Nota: Archives Springer e-books (Licence nationale)
Archives Springer e-books (Licence nationale)
Autres localisations: Voir dans le Sudoc
Edition sous un autre format:• Types for proofs and programs, international workshop, TYPES 2002, Berg en Dal, the Netherlands, April 24-28, 2002, selected papers, Herman Geuvers, Freek Wiedijk (eds.), Berlin, Springer, 2003, 1 vol. (VIII-330 p.), Lecture notes in computer science, 3-540-14031-X
• Types for Proofs and Programs, Texte imprimé, 9783662213414
Taula de continguts:
  • (Co-)Iteration for Higher-Order Nested Datatypes
  • Program Extraction in Simply-Typed Higher Order Logic
  • General Recursion in Type Theory
  • Using Theory Morphisms for Implementing Formal Methods Tools
  • Subsets, Quotients and Partial Functions in Martin-Löf s Type Theory
  • Mathematical Quotients and Quotient Types in Coq
  • A Constructive Formalization of the Fundamental Theorem of Calculus
  • Two Behavioural Lambda Models
  • A Unifying Approach to Recursive and Co-recursive Definitions
  • Holes with Binding Power
  • Typing with Conditions and Guarantees for Functional In-place Update
  • A New Extraction for Coq
  • Weak Transitivity in Coercive Subtyping
  • The Not So Simple Proof-Irrelevant Model of CC
  • Structured Proofs in Isar/HOL
  • Java as a Functional Programming Language
  • Monad Translating Inductive and Coinductive Types
  • A Finite First-Order Presentation of Set Theory.

Ítems similars