Zobrazeno 1 - 10 of 21 pro vyhledávání: '"Ana Bove"'
1
Modelling general recursion in type theory
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
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::a01da0472f190a809ce4dbbf8f45db99
https://doi.org/10.1017/s0960129505004822
Zobrazit plný text záznamu
2
Partiality and Recursion in Interactive Theorem Provers - An Overview
Autor: Alexander Krauss, Ana Bove, Matthieu Sozeau
Publikováno v: Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, 2012
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2012
To appear; International audience; The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalising mathematics is becoming more common and feasible in practice. However, most mature t
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bc5fed82769de9784dd95f258025b170
https://inria.hal.science/hal-00691459/document
Zobrazit plný text záznamu
3
Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs
Autor: Andrés Sicard-Ramírez, Ana Bove, Peter Dybjer
Publikováno v: Foundations of Software Science and Computational Structures ISBN: 9783642287282
FoSSaCS
We propose a new approach to the computer-assisted verification of functional programs. We work in first order theories of functional programs which are obtained by extending Aczel's first order theory of combinatory formal arithmetic with positive i
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::67ac590ba521dfc44884069abc7473c2
https://doi.org/10.1007/978-3-642-28729-9_7
Zobrazit plný text záznamu
4
Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers
Autor: Milad Niqui, Ekaterina Komendantskaya, Ana Bove
Publikováno v: Electronic Proceedings in Theoretical Computer Science. 43
htmlabstractThis volume contains the proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010) which took place on July 15 in Edinburgh, UK. This workshop was held as a satellite workshop of the International C
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::283bc67b1f8186a933d346f2d59fed29
https://doi.org/10.4204/eptcs.43.0
Zobrazit plný text záznamu
5
Embedding a logical theory of constructions in Agda
Autor: Andrés Sicard-Ramírez, Ana Bove, Peter Dybjer
Publikováno v: PLPV
We propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-Lof's intuitionistic type theory. We show how to embed an external programming logic, Aczel's Logi
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::caa7f3d3a9a29bf48ce625b94147d95f
https://doi.org/10.1145/1481848.1481857
Zobrazit plný text záznamu
6
Dependent Types at Work
Autor: Ana Bove, Peter Dybjer
Publikováno v: Language Engineering and Rigorous Software Development ISBN: 9783642031526
LerNet ALFA Summer School
In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is an extension of Martin-Lof type theory. First we show how to do simply typed functional pro
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b37dcbd41ddab678292c7fe5b5a05aab
https://doi.org/10.1007/978-3-642-03153-3_2
Zobrazit plný text záznamu
7
A Brief Overview of Agda – A Functional Language with Dependent Types
Autor: Ana Bove, Peter Dybjer, Ulf Norell
Publikováno v: Lecture Notes in Computer Science ISBN: 9783642033582
TPHOLs
We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-Lof's intuitionistic type theory but extends it with numerous programming language features. It supports a
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::8affdbb315f68b673fdbbf013c1862cc
https://doi.org/10.1007/978-3-642-03359-9_6
Zobrazit plný text záznamu
9
A Type of Partial Recursive Functions
Autor: Venanzio Capretta, Ana Bove
Publikováno v: Lecture Notes in Computer Science ISBN: 9783540710653
TPHOLs
Our goal is to define a type of partial recursive functions in constructive type theory. In a series of previous articles, we studied two different formulations of partial functions and general recursion. We could obtain a type only by extending the
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::94532cc67cb2861bc5b5b17501835303
https://doi.org/10.1007/978-3-540-71067-7_12
Zobrazit plný text záznamu
10
Computation by Prophecy
Autor: Ana Bove, Venanzio Capretta
Publikováno v: Lecture Notes in Computer Science ISBN: 9783540732273
TLCA
We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that characterises the traces of the computation of the function. The structure of a proph
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::99cd4399469d1ada643bc0fc719c8c44
https://doi.org/10.1007/978-3-540-73228-0_7
Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání

Omezení vyhledávání
Plný text Recenzováno Digitální knihovna AV ČR
Zdroje