|
| volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 1 van 3 gevonden artikelen
| Titel: |
An Introduction to Programming and Proving with Dependent Types in Coq |
| Auteur: |
Adam Chlipala |
| Verschenen in: |
Journal of formalized reasoning |
| Paginering: | Jaargang 3 (2010) nr. 2 pagina's 1-93 |
| Jaar: |
2010 |
| Inhoud: |
Computer proof assistants vary along many dimensions. Among the mature implementations, the Coq system is distinguished by two key features. First, we have support for programming with dependent types in the tradition of type theory, based on dependent function types and inductive type families. Second, we have a domain-specific language for coding correct-by-construction proof automation. Though the Coq user community has grown quite large, neither of the aspects I highlight is widely used. In this tutorial, I aim to provide a pragmatic introduction to both, showing how they can bring significant improvements in productivity. |
| Uitgever: |
CIB - University of Bologna (provided by DOAJ) |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 1 van 3 gevonden artikelen
| volgende >> |