Benjamin Werner

Citado por

	Todos	Desde 2020
Citações	2614	487
Índice h	23	11
Índice i10	29	11

120

199219931994199519961997199819992000200120022003200420052006200720082009201020112012201320142015201620172018201920202021202220232024202512 27 36 34 54 75 63 80 72 96 63 78 74 93 78 100 97 66 93 113 98 89 94 76 80 76 69 101 86 93 76 117 97 18

Coautores

Christine PAULIN-MOHRINGLMF, Université Paris-SaclayE-mail confirmado em universite-paris-saclay.fr
Jean-Christophe FilliâtreCNRSE-mail confirmado em lri.fr
Gérard HuetDirecteur de Recherche Emérite InriaE-mail confirmado em inria.fr
Cesar MunozNASAE-mail confirmado em nasa.gov
Benjamin GregoireInria Sophia-AntipolisE-mail confirmado em inria.fr
Stephane GaubertDirecteur de recherche, INRIA and CMAP, Ecole polytechniqueE-mail confirmado em inria.fr
Victor MagronCNRSE-mail confirmado em laas.fr
David DelahayeE-mail confirmado em cnam.fr
Georges GonthierPrincipal Researcher, Microsoft ResearchE-mail confirmado em microsoft.com
François GarillotE-mail confirmado em garillot.net
Herman GeuversRadboud University Nijmegen, the NetherlandsE-mail confirmado em cs.ru.nl
Paul-André MellièsCNRS, Université Paris CitéE-mail confirmado em irif.fr
Martin AbadiResearch Scientist, Google, and Professor Emeritus, UC Santa CruzE-mail confirmado em cs.ucsc.edu
Pierre-Yves StrubResearch Scientist, PQShieldE-mail confirmado em strub.nu
Roberto Di CosmoProfessor of Computer Science, University Paris DiderotE-mail confirmado em dicosmo.org
Arnaud SpiwackDirector, Research, Tweag & Modus CreateE-mail confirmado em spiwack.net

Seguir

Benjamin Werner

Professeur, Computer Science, Ecole Polytechnique

E-mail confirmado em polytechnique.edu - Página inicial

Logic computer science type theory formal proofs Coq


Título Ordenar por citações Ordenar por ano Ordenar por título	Citado por Citado por	Ano
The coq proof assistant, reference manual, version 5.10 C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Munoz, C Murthy, ... INRIA, 1995	430*	1995
Une théorie des constructions inductives B Werner Université Paris-Diderot-Paris VII, 1994	353	1994
Verifying SAT and SMT in Coq for a fully automated decision procedure M Armand, G Faure, B Grégoire, C Keller, L Théry, B Werner	258*	2011
Synthesis of ML programs in the system Coq C Paulin-Mohring, B Werner Journal of Symbolic Computation 15 (5-6), 607-640, 1993	186	1993
Sets in types, types in sets B Werner International Symposium on Theoretical Aspects of Computer Software, 530-546, 1997	147	1997
The Coq proof assistant user's guide: version 5.8 G Dowek, A Felty, H Herbelin, G Huet, C Parent, C Paulin-Mohring, ... INRIA, 1993	140	1993
The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 17-21, 1999	137	1999
Proof normalization modulo G Dowek, B Werner The Journal of Symbolic Logic 68 (04), 1289-1316, 2003	136	2003
Arithmetic as a theory modulo G Dowek, B Werner International Conference on Rewriting Techniques and Applications, 423-437, 2005	82	2005
Importing HOL light into Coq C Keller, B Werner International Conference on Interactive Theorem Proving, 307-322, 2010	73	2010
The Coq proof assistant reference manual C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Paulin-Mohring, ... Rapport Technique 177, 1995	62	1995
Proof normalization modulo G Dowek, B Werner Types for Proofs and Programs: International Workshop, TYPES’98 Kloster …, 1999	46	1999
The not so simple proof-irrelevant model of CC A Miquel, B Werner Types for Proofs and Programs: International Workshop, TYPES 2002, Berg en …, 2003	45	2003
On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study H Geuvers, B Werner Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 320-329, 1994	44	1994
A generic normalisation proof for pure type systems PA Mellies, B Werner International Workshop on Types for Proofs and Programs, 254-276, 1996	42	1996
A computational approach to pocklington certificates in type theory B Grégoire, L Théry, B Werner International Symposium on Functional and Logic Programming, 97-113, 2006	39	2006
On the strength of proof-irrelevant type theories B Werner Logical Methods in Computer Science 4, 2008	38	2008
Simple types in type theory: Deep and shallow encodings F Garillot, B Werner International Conference on Theorem Proving in Higher Order Logics, 368-382, 2007	37	2007
Formal proofs for nonlinear optimization X Allamigeon, S Gaubert, V Magron, B Werner ArXiv e-prints 1404, 2014	35*	2014
A normalization proof for an impredicative type system with large elimination over integers B Werner, B Nordström, K Petersson, G Plotkin International Workshop on Types for Proofs and Programs (TYPES), 341-357, 1992	32	1992

O sistema não pode executar a operação agora. Tente novamente mais tarde.

Artigos 1–20

Citações por ano

Citações duplicadas

Citações mescladas

Adicionar coautoresCoautores

Seguir

Citado por

Coautores