Théo Winterhalter

Publications

230

Citations

H-Index

2017

Active since

Affiliations

Institut national de recherche en sciences et technologies du numérique(Current)

Centre Inria de l'Université de Rennes

Saarland University

Laboratoire des Sciences du Numérique de Nantes

Max Planck Institute for Security and Privacy

Théo Winterhalter is an author at Institut national de recherche en sciences et technologies du numérique specializing in automated reasoning, engineering, and formal verification.

ORCID

Top concepts

EngineeringAutomated ReasoningFormal MethodsComputer ScienceFormal VerificationVerificationProgram AnalysisSoftware AnalysisFormal SpecificationCompilers

Publications per year

2017–2023

Publications

The MetaCoq Project

Matthieu Sozeau, Abhishek Anand, Simon Boulier et al. · Journal of Automated Reasoning · 2020 · 71 citations

Engineering, Graph Query Language, Very Large Database +6

Coq Coq correct! verification of type checking and erasure for Coq, in Coq

Matthieu Sozeau, Simon Boulier, Yannick Forster et al. · Proceedings of the ACM on Programming Languages · 2019 · 60 citations · Full text

Engineering, Coq Definitions, Type Theory +18

Normalization by evaluation for sized dependent types

Andreas Abel, Andrea Vezzosi, Théo Winterhalter · Proceedings of the ACM on Programming Languages · 2017 · 26 citations · Full text

Mathematical Programming, Engineering, Type Theory +18

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas et al. · 2021 · 21 citations

Cryptographic Primitive, Engineering, Verification +18

The taming of the rew: a type theory with computational assumptions

Jesper Cockx, Nicolas Tabareau, Théo Winterhalter · Proceedings of the ACM on Programming Languages · 2021 · 20 citations · Full text

Engineering, Type Theory, Verification +16

Rows per page

1–5 of 7