Robert Y. Lewis

20 papers B 5C 1Journal 11Unranked 3
YearRankTypeTitle / Venue / Authors
2025 — conf
KLean: Extending Operating System Kernels with Lean.
PLOS@SOSP
Di Jin, Ethan Lavi, Jinghao Jia, Robert Y. Lewis, Nikos Vasilakis
2024 J jnl
Formalized Functional Analysis with Semilinear Maps.
J. Autom. Reason.
Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth
2022 J jnl
A Bi-Directional Extensible Interface Between Lean and Mathematica.
J. Autom. Reason.
Robert Y. Lewis, Minchao Wu
2022 B conf
Formalized functional analysis with semilinear maps.
ITP
Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth
2022 J jnl
Formalized functional analysis with semilinear maps.
CoRR
Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth
2021 J jnl
A bi-directional extensible interface between Lean and Mathematica.
CoRR
Robert Y. Lewis, Minchao Wu
2021 B conf
Formalizing the ring of Witt vectors.
CPP
Johan Commelin, Robert Y. Lewis
2020 J jnl
Formalizing the Ring of Witt Vectors.
CoRR
Johan Commelin, Robert Y. Lewis
2020 C conf
Maintaining a Library of Formal Mathematics.
CICM
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
2020 J jnl
Maintaining a Library of Formal Mathematics.
CoRR
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
2020 J jnl
Normalizing Casts and Coercions.
CoRR
Robert Y. Lewis, Paul-Nicolas Madelaine
2020 — conf
Simplifying Casts and Coercions (Extended Abstract).
PAAR+SC²@IJCAR
Robert Y. Lewis, Paul-Nicolas Madelaine
2019 J jnl
A formal proof of Hensel's lemma over the p-adic integers.
CoRR
Robert Y. Lewis
2019 B conf
A formal proof of hensel's lemma over the p-adic integers.
CPP
Robert Y. Lewis
2019 B conf
Formalizing the Solution to the Cap Set Problem.
ITP
Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis
2019 J jnl
Formalizing the Solution to the Cap Set Problem.
CoRR
Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis
2017 — conf
An Extensible Ad Hoc Interface between Lean and Mathematica.
PxTP
Robert Y. Lewis
2016 J jnl
A Heuristic Prover for Real Inequalities.
J. Autom. Reason.
Jeremy Avigad, Robert Y. Lewis, Cody Roux
2014 B conf
A Heuristic Prover for Real Inequalities.
ITP
Jeremy Avigad, Robert Y. Lewis, Cody Roux
2014 J jnl
A heuristic prover for real inequalities.
CoRR
Jeremy Avigad, Robert Y. Lewis, Cody Roux