Filtrer vos résultats
- 198
- 52
- 105
- 67
- 26
- 19
- 8
- 4
- 4
- 4
- 3
- 3
- 2
- 2
- 1
- 1
- 1
- 4
- 2
- 209
- 70
- 2
- 1
- 1
- 1
- 3
- 16
- 8
- 12
- 24
- 28
- 37
- 19
- 30
- 16
- 10
- 20
- 3
- 16
- 6
- 1
- 1
- 230
- 16
- 4
- 150
- 148
- 112
- 102
- 20
- 18
- 15
- 13
- 11
- 9
- 9
- 8
- 7
- 6
- 6
- 5
- 5
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 31
- 25
- 20
- 16
- 14
- 12
- 11
- 10
- 9
- 9
- 9
- 8
- 7
- 7
- 6
- 6
- 6
- 6
- 6
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
250 résultats
|
|
The Many-Worlds Calculus2022
Pré-publication, Document de travail
hal-03654190v2
|
||
|
|
Linear Haskell: practical linearity in a higher-order polymorphic languageProceedings of the ACM on Programming Languages, 2017, 2 (POPL), pp.1-29. ⟨10.1145/3158093⟩
Article dans une revue
hal-01673536v1
|
||
|
|
Extending Type Theory with ForcingLICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0
Communication dans un congrès
hal-00685150v1
|
||
|
|
Towards Certified Meta-Programming with Typed Template-CoqITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.20-39, ⟨10.1007/978-3-319-94821-8_2⟩
Communication dans un congrès
hal-01809681v1
|
||
Incremental Update for Graph RewritingEuropean Symposium on Programming (ESOP), Apr 2017, Uppsala, Sweden. ⟨10.1007/978-3-662-54434-1_8⟩
Communication dans un congrès
hal-02357978v1
|
|||
|
|
Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculusWorkshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. pp.209-217
Communication dans un congrès
inria-00381554v1
|
||
|
|
The complexity of satisfaction problems in reverse mathematicsComputability, 2015, 4 (1), pp.69-84
Article dans une revue
hal-01888582v1
|
||
|
|
Reduction Operators and Completion of Rewriting SystemsJournal of Symbolic Computation, In press
Article dans une revue
hal-01325907v2
|
||
|
|
Formal Proof of Banach-Tarski ParadoxJournal of Formalized Reasoning, 2017, 10 (1), pp.37-49. ⟨10.6092/issn.1972-5787/6927⟩
Article dans une revue
hal-01673378v1
|
||
|
|
De nouveaux outils pour calculer avec des inductifs en CoqLangage de programmation [cs.PL]. Université Paris-Diderot - Paris VII, 2014. Français. ⟨NNT : ⟩
Thèse
tel-01054723v1
|
||
|
|
Towards typed repositories of proofsMathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France
Communication dans un congrès
inria-00525874v1
|
||
|
|
Constructive completeness for the linear-time µ-calculusConference on Logic in Computer Science 2017, Jun 2017, Reykjavik, Iceland
Communication dans un congrès
hal-01430737v1
|
||
|
|
Models of a Non-Associative CompositionFOSSACS 2014 - 17th International Conference on Foundations of Software Science and Computation Structures, Apr 2014, Grenoble, France. pp.396-410, ⟨10.1007/978-3-642-54830-7_26⟩
Communication dans un congrès
hal-00996729v1
|
||
Local validity for circular proofs in linear logic with fixed points: extended versionComputer Science Logic, Sep 2018, Birmingham, United Kingdom
Communication dans un congrès
hal-01825477v1
|
|||
|
|
Correlating OraclesLogiciel hal-01831369v2 |
||
|
|
λμ-calculus and Λμ-calculus: a Capital Difference2009
Pré-publication, Document de travail
inria-00524942v1
|
||
|
|
Equality is typable in Semi-Full Pure Type SystemsLogic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. 10 p
Communication dans un congrès
inria-00496988v1
|
||
|
|
Pure Type System conversion is always typableJournal of Functional Programming, 2012, 22 (2), pp.153 - 180. ⟨10.1017/S0956796812000044⟩
Article dans une revue
inria-00497177v2
|
||
|
|
A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuseThe Coq Workshop, Jul 2021, Virtual, France
Document associé à des manifestations scientifiques
hal-03366644v1
|
||
|
|
Challenges in the collaborative evolution of a proof language and its ecosystemSoftware Engineering [cs.SE]. Université Paris Cité, 2019. English. ⟨NNT : 2019UNIP7163⟩
Thèse
tel-02451322v1
|
||
CrowdsourcingMarie Cornu, Fabienne Orsi, Judith Rochfeld. Dictionnaire des biens communs, PUF Quadrige, pp.333-336, 2017, 978-2130654117
Chapitre d'ouvrage
hal-03914562v1
|
|||
|
|
A Foundational Framework for the Specification and Verification of Mechanism DesignEC'22 - Twenty-Third ACM Conference on Economics and Computation, Jul 2022, Colorado, United States.
Poster de conférence
hal-03715847v1
|
||
|
|
Inferring types for functional methods (where method calls come for free)2004
Pré-publication, Document de travail
hal-01149745v1
|
||
|
|
Coq Community Survey 2022: Summary of ResultsDocument associé à des manifestations scientifiques hal-03914602v1 |
||
Universe Polymorphism in CoqInteractive Theorem Proving, Jul 2014, Vienna, Austria
Communication dans un congrès
hal-00974721v1
|
|||
|
|
OCaml étendu avec du filtrage par comotifsJFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls sur mer, France
Communication dans un congrès
hal-01897456v1
|
||
|
|
Realizability games for arithmetical formulæWorskshop GaLoP2015, Apr 2015, Londres, United Kingdom
Communication dans un congrès
hal-01248093v1
|
||
|
|
Oracle-based Differential Operational Semantics (long version)[Research Report] Université Paris Diderot / Sorbonne Paris Cité. 2016
Rapport
hal-01419860v1
|
||
|
|
Certifying cost annotations in compilers2010
Rapport
hal-00524715v1
|
||
|
|
Revisiting the categorical interpretation of dependent type theoryTheoretical Computer Science, 2014, 546, pp.99-119. ⟨10.1016/j.tcs.2014.03.003⟩
Article dans une revue
hal-01114033v1
|