Filtrer vos résultats
- 9
- 1
- 6
- 1
- 1
- 1
- 1
- 1
- 10
- 1
- 1
- 1
- 2
- 1
- 3
- 1
- 9
- 1
- 3
- 3
- 3
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 10
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
10 résultats
|
|
|
triés par
|
|
|
Functors for Proofs and Programs13th European Symposium on Programming, ESOP 2004, Feb 2004, Barcelona, Spain. pp.370-384, ⟨10.1007/b96702⟩
Communication dans un congrès
hal-00150913v1
|
||
|
|
Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant CoqAutre [cs.OH]. Université Paris Sud - Paris XI, 2004. Français. ⟨NNT : ⟩
Thèse
tel-00150912v1
|
||
|
|
Formalizing Stalmarck's algorithm in CoqTheorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, 2000, Portland, United States. pp.388
Communication dans un congrès
hal-00150915v1
|
||
|
|
A New Extraction for CoqTypes for Proofs and Programs: International Workshop, TYPES 2002, Feb 2004, Berg en Dal, Netherlands. pp.617
Communication dans un congrès
hal-00150914v1
|
||
Coq 8.4 Reference Manual[Research Report] Inria. 2014
Rapport
hal-01114602v1
|
|||
|
|
A Large-Scale Experiment in Executing Extracted ProgramsCalculemus 2005, Mar 2006, Newcastle upon Tyne, United Kingdom. pp.75-91, ⟨10.1016/j.entcs.2005.11.024⟩
Communication dans un congrès
hal-00150908v1
|
||
|
|
Extraction in Coq, an OverviewLogic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, Jun 2008, Athens, Greece. ⟨10.1007/978-3-540-69407-6⟩
Communication dans un congrès
hal-00338973v1
|
||
|
|
Program extraction from normalization proofsStudia Logica, 2006, 82 (1), pp.25-49. ⟨10.1007/s11225-006-6604-5⟩
Article dans une revue
istex
hal-00150904v1
|
||
|
|
Rough Pearl: Manufacturing Cons-Cells35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
Communication dans un congrès
hal-04406422v1
|
||
|
|
Implicit and noncomputational arguments using monads2005
Pré-publication, Document de travail
hal-00150900v1
|