Zobrazeno 1 - 10
of 31
pro vyhledávání: '"Venanzio Capretta"'
Autor:
Venanzio Capretta
Publikováno v:
Logical Methods in Computer Science, Vol Volume 1, Issue 2 (2005)
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of ope
Externí odkaz:
https://doaj.org/article/04d7650f0ffb42b8b3f1b58fe1a82fa6
This Festschrift, dedicated to Herman Geuvers on the occasion of his 60th birthday, contains papers written by many of his closest collaborators. Herman Geuvers is a full professor at Radboud University Nijmegen and holds a part-time professorship at
Autor:
Venanzio Capretta, Colm Baston
Publikováno v:
Interactive Theorem Proving ISBN: 9783319948201
ITP
ITP
We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rathe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d35b7d0099ac4136968776cbf897b208
https://doi.org/10.1007/978-3-319-94821-8_8
https://doi.org/10.1007/978-3-319-94821-8_8
Publikováno v:
IFL
Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they
Autor:
Tarmo Uustalu, Venanzio Capretta
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783662496299
FoSSaCS
FoSSaCS
We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover certain classically valid theorems in a constructive setting. It is a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f8cc90a1dbaf39f12e72512da9ae12f1
https://doi.org/10.1007/978-3-662-49630-5_6
https://doi.org/10.1007/978-3-662-49630-5_6
Autor:
Ana Bove, Venanzio Capretta
Publikováno v:
Mathematical Structures in Computer Science. 15:671-708
Constructive type theory is an expressive programming language in which both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only terminating programs can be defined in it. Hence, g
Publikováno v:
CMCS
Information and Computation, 71, 437-468
Information and Computation, 71, 4, pp. 437-468
Information and Computation, 71, 437-468
Information and Computation, 71, 4, pp. 437-468
The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the u
Publikováno v:
Journal of Functional Programming. 13:261-293
Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for develop
Publikováno v:
Linguistics and Philosophy. 24:531-595
The prime purpose of this paper is, first, to restore to discourse-bound occasion sentences their rightful central place in semantics and secondly, taking these as the basic propositional elements in the logical analysis of language, to contribute to
Autor:
Venanzio Capretta, Silvio Valentini
Publikováno v:
Mathematical Structures in Computer Science. 9:719-739
In this paper we describe a method for proving the normalization property for a large variety of typed lambda calculi of first and second order, which is based on a proof of equivalence of two deduction systems. We first illustrate the method on the