Skip to Main content Skip to Navigation

inria-00497177v2  Journal articles
Vincent SilesHugo Herbelin. Pure Type System conversion is always typable
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (2), pp.153 - 180. ⟨10.1017/S0956796812000044⟩
hal-00779752v1  Conference papers
Pierre-Marie Pédrot. Un régime au concentré d'automate
JFLA - Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France
hal-00548167v1  Conference papers
Noam Zeilberger. Polarity and the Logic of Delimited Continuations
25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Jul 2010, Edinburgh, United Kingdom. pp.219 - 227, ⟨10.1109/LICS.2010.23⟩
inria-00481815v1  Conference papers
Hugo Herbelin. An intuitionistic logic that proves Markov's principle
Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. pp.50-56
hal-00816918v1  Preprints, Working Papers, ...
Pierre Boutillier. Simple simpl
hal-01105252v1  Conference papers
Marc Lasson. Canonicity of Weak ω-groupoid Laws Using Parametricity Theory
MFPS 2014, Jun 2014, Ithaca, United States. pp.229 - 244, ⟨10.1016/j.entcs.2014.10.013⟩
hal-00690270v1  Conference papers
Federico AschieriMargherita Zorzi. Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability
Classical Logic and Computation 2012, Jul 2012, Warwick, United Kingdom. ⟨10.4204/EPTCS.97.1⟩
hal-01111193v1  Conference papers
Beta ZilianiMatthieu Sozeau. Towards a better-behaved unification algorithm for Coq
UNIF 2014 Workshop, Jul 2014, Vienna, Austria. pp 74--87
hal-01110337v1  Conference papers
Alexis SaurinPierre-Marie Pédrot. Nécessité faite loi: de la réduction linéaire de tête à l'évaluation paresseuse.
JFLA 2014 - Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Jan 2014, Fréjus, France
hal-01111802v1  Conference papers
Pierre-Marie Pédrot. A Functional Functional Interpretation
CSL-LICS 2014 - Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603094⟩
hal-01250855v1  Master thesis
Cyprien Mangin. Eliminating Dependent Pattern-Matching in Coq
Programming Languages [cs.PL]. 2015
inria-00409793v2  Conference papers
Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability (version with appendices)
18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. pp.409-423, ⟨10.1007/978-3-642-04027-6_30⟩
inria-00491236v2  Conference papers
Pierre-Louis CurienGuillaume Munch-Maccagnoni. The Duality of Computation under Focus
6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. pp.165-181, ⟨10.1007/978-3-642-15240-5_13⟩
tel-00529021v1  Theses
Danko Ilik. Constructive Completeness Proofs and Delimited Control
Software Engineering [cs.SE]. Ecole Polytechnique X, 2010. English
hal-02292537v1  Reports
Guillaume Claret. OPAM for Coq
[Technical Report] Inria - Paris 7. 2015
hal-01195587v4  Reports
Pierre Letouzey. Hofstadter's problem for curious readers
[Research Report] Université Paris Diderot; INRIA Paris-Rocquencourt. 2015, pp.29
hal-00651780v1  Conference papers
Pierre Boutillier. A relaxation of Coq's guard condition
JFLA - Journées Francophones des langages applicatifs - 2012, Feb 2012, Carnac, France. pp.1 - 14
hal-00697065v1  Conference papers
Pierre-Louis Curien. Operads, clones, and distributive laws
Operads and Universal Algebra : Proceedings of China-France Summer Conference, Jul 2010, Tianjin, China. pp.25-50
hal-00699581v1  Conference papers
Matthieu Sozeau. Elaborations in Type Theory
DTP'10 - Dependently Typed Programming - 2010, Jul 2010, Edinburgh, United Kingdom
hal-00699595v1  Conference papers
Matthieu Sozeau. Coq avec Classes
JFLA - Journées Françaises des Langages Applicatifs, Feb 2012, Carnac, France
hal-00426228v2  Journal articles
Yves GuiraudPhilippe Malbos. Identities among relations for higher-dimensional rewriting systems
Séminaires et congrès, Société mathématique de France, 2013, 26, pp.145-161
hal-00818253v1  Conference papers
Yves GuiraudPhilippe MalbosSamuel Mimram. A Homotopical Completion Procedure with Applications to Coherence of Monoids
RTA - 24th International Conference on Rewriting Techniques and Applications - 2013, Jun 2013, Eindhoven, Netherlands. pp.223-238, ⟨10.4230/LIPIcs.RTA.2013.223⟩
hal-00470795v2  Journal articles
Yves GuiraudPhilippe Malbos. Coherence in monoidal track categories
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2012, 22 (6), pp.931-969. ⟨10.1017/S096012951100065X⟩
hal-00531242v3  Journal articles
Yves GuiraudPhilippe Malbos. Higher-dimensional normalisation strategies for acyclicity
Advances in Mathematics, Elsevier, 2012, 231 (3-4), pp.2294-2351. ⟨10.1016/j.aim.2012.05.010⟩
hal-00682233v4  Journal articles
Stéphane GaussentYves GuiraudPhilippe Malbos. Coherent presentations of Artin monoids
Compositio Mathematica, Foundation Compositio Mathematica, 2015, 151 (5), pp.957-998. ⟨10.1112/S0010437X14007842⟩