Aleksey Nogin
Aleksey Nogin
Senior Computer Scientist at HRL Laboratories, LLC
Zweryfikowany adres z hrl.com - Strona główna
Tytuł
Cytowane przez
Cytowane przez
Rok
MetaPRL–A Modular Logical Environment
J Hickey, A Nogin, R Constable, B Aydemir, E Barzilay, Y Bryukhov, ...
Theorem Proving in Higher Order Logics, 287-303, 2003
672003
Synaptic time multiplexing neuromorphic network that forms subsets of connections during different time slots
JM Cruz-Albrecht, N Srinivasa, P Petre, Y Cho, A Nogin
US Patent 8,977,578, 2015
652015
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants
S Schmitt, L Lorigo, C Kreitz, A Nogin
Lecture Notes in Computer Science, 421-426, 2001
592001
HRLSim: a high performance spiking neural network simulator for GPGPU clusters
K Minkovich, CM Thibeault, MJ O'Brien, A Nogin, Y Cho, N Srinivasa
IEEE transactions on neural networks and learning systems 25 (2), 316-331, 2013
542013
Programming Time-Multiplexed Reconfigurable Hardware Using a Scalable Neuromorphic Compiler
K Minkovich, N Srinivasa, JM Cruz-Albrecht, Y Cho, A Nogin
IEEE Transactions on Neural Networks and Learning Systems, 2012
382012
Quotient types: A modular approach
A Nogin
International Conference on Theorem Proving in Higher Order Logics, 263-280, 2002
342002
Sequent schema for derived rules
A Nogin, J Hickey
International Conference on Theorem Proving in Higher Order Logics, 281-297, 2002
342002
MetaPRL home page
JJ Hickey, A Nogin, A Kopylov
27
Markov’s principle for propositional type theory
A Kopylov, A Nogin
Computer Science Logic, 570-584, 2001
242001
Fast tactic-based theorem proving
J Hickey, A Nogin
International Conference on Theorem Proving in Higher Order Logics, 252-267, 2000
242000
A verified messaging system
W Mansky, AW Appel, A Nogin
Proceedings of the ACM on Programming Languages 1 (OOPSLA), 1-28, 2017
202017
A listing of MetaPRL theories
J Hickey, B Aydemir, Y Bryukhov, A Kopylov, A Nogin, X Yu.
19*
Formal compiler construction in a logical framework
J Hickey, A Nogin
Higher-order and symbolic computation 19 (2), 197-230, 2006
152006
System and methods for digital artifact genetic modeling and forensic analysis
TC Lu, H Moon, GD Holland, DL Allen, A Nogin, MD Howard
US Patent 9,224,067, 2015
142015
A computational approach to reflective meta-reasoning about languages with bindings
A Nogin, A Kopylov, X Yu, J Hickey
Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized Reasoning about …, 2005
142005
Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
J Hickey, A Nogin, X Yu, A Kopylov
ACM SIGPLAN Notices 41 (9), 172-183, 2006
122006
Theory and implementation of an efficient tactic-based logical framework
AY Nogin
Cornell University, 2002
122002
Writing constructive proofs yielding efficient extracted programs
A Nogin
Electronic Notes in Theoretical Computer Science 37, 1-17, 2000
122000
Formalizing Type Operations Using the “Image” Type Constructor
A Nogin, A Kopylov
Electronic Notes in Theoretical Computer Science 165, 121-132, 2006
112006
OMake: Designing a scalable build process
J Hickey, A Nogin
International Conference on Fundamental Approaches to Software Engineering …, 2006
112006
Nie można teraz wykonać tej operacji. Spróbuj ponownie później.
Prace 1–20