Jason Gross
Citeras av
Citeras av
One shot learning of simple visual concepts
B Lake, R Salakhutdinov, J Gross, J Tenenbaum
Proceedings of the annual meeting of the cognitive science society 33 (33), 2011
Measuring the human retinal oxygenation response to a hyperoxic challenge using MRI: eliminating blinking artifacts and demonstrating proof of concept
BA Berkowitz, C McDonald, Y Ito, PS Tofts, Z Latif, J Gross
Magnetic Resonance in Medicine: An Official Journal of the International …, 2001
Fiat: Deductive synthesis of abstract data types in a proof assistant
B Delaware, C Pit-Claudel, J Gross, A Chlipala
ACM SIGPLAN Notices 50 (1), 689-700, 2015
The HoTT library: a formalization of homotopy type theory in Coq
A Bauer, J Gross, PLF Lumsdaine, M Shulman, M Sozeau, B Spitters
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
Simple high-level code for cryptographic arithmetic-with proofs, without compromises
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
2019 IEEE Symposium on Security and Privacy (SP), 1202-1219, 2019
Experience implementing a performant category-theory library in Coq
J Gross, A Chlipala, DI Spivak
International Conference on Interactive Theorem Proving, 275-291, 2014
The end of history? Using a proof assistant to replace language design with library design
A Chlipala, B Delaware, S Duchovni, J Gross, C Pit-Claudel, S Suriyakarn, ...
2nd Summit on Advances in Programming Languages (SNAPL 2017), 2017
The HoTT library
A Bauer, J Gross, PLF Lumsdaine, M Shulman, B Spitters
URL: https://github. com/HoTT/HoTT, 2016
Systematic generation of fast elliptic curve cryptography implementations
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
Technical Report. https://people. csail. mit. edu/jgross/personal-website …, 2018
Persistence diagrams as diagrams: A categorification of the stability theorem, 2016
U Bauer, M Lesnick
arXiv preprint arXiv:1610.10085, 0
Reification by Parametricity
J Gross, A Erbsen, A Chlipala
International Conference on Interactive Theorem Proving, 289-305, 2018
The Speed and Lifetime of Cosmic-Ray Muons
J Gross
MIT, 2011
An extensible framework for synthesizing efficient, verified parsers
JS Gross
Massachusetts Institute of Technology, 2015
Systematic Synthesis of Elliptic Curve Cryptography Implementations
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
The Metaphysics of Music
JM Gross
Löb’s Theorem
J Gross, J Gallagher, B Fallenstein
Simple High-Level Code For Cryptographic Arithmetic–With Proofs, Without Compromises
AEJ Philipoom, JGRSA Chlipala
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
C Pit-Claudel, P Wang, B Delaware, J Gross, A Chlipala
Parsing Parses
J Gross, A Chlipala
A Computational Interpretation of Higher Inductive Types: How to Tame Equality in your Types
J Gross
Systemet kan inte utföra åtgärden just nu. Försök igen senare.
Artiklar 1–20