Aleksey Nogin
Aleksey Nogin
Head of Research, Red Balloon Security
Verified email at - Homepage
Cited by
Cited by
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
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
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
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
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
Quotient types: A modular approach
A Nogin
International Conference on Theorem Proving in Higher Order Logics, 263-280, 2002
Sequent schema for derived rules
A Nogin, J Hickey
International Conference on Theorem Proving in Higher Order Logics, 281-297, 2002
MetaPRL home page
JJ Hickey, A Nogin, A Kopylov
Markov’s principle for propositional type theory
A Kopylov, A Nogin
Computer Science Logic, 570-584, 2001
Fast tactic-based theorem proving
J Hickey, A Nogin
International Conference on Theorem Proving in Higher Order Logics, 252-267, 2000
A verified messaging system
W Mansky, AW Appel, A Nogin
Proceedings of the ACM on Programming Languages 1 (OOPSLA), 1-28, 2017
A listing of MetaPRL theories
J Hickey, B Aydemir, Y Bryukhov, A Kopylov, A Nogin, X Yu.
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
Formal compiler construction in a logical framework
J Hickey, A Nogin
Higher-order and symbolic computation 19 (2), 197-230, 2006
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
Writing constructive proofs yielding efficient extracted programs
A Nogin
Electronic Notes in Theoretical Computer Science 37, 1-17, 2000
Formalizing Type Operations Using the “Image” Type Constructor
A Nogin, A Kopylov
Electronic Notes in Theoretical Computer Science 165, 121-132, 2006
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
Theory and Implementation of an Efficient Tactic-Based Logical Framework.
A Nogin
Cornell University, 2002
Establishing Common Interest Negotiation Links Between Consumers and Suppliers to Facilitate Solving a Resource Allocation Problem
DW Payton, A Nogin
US Patent App. 12/702,062, 2010
The system can't perform the operation now. Try again later.
Articles 1–20