Fast Tactic-Based Theorem Proving. - Jason Hickey; Aleksey Nogin (TPHOLs, 2000)

Writing Constructive Proofs Yielding Efficient Extracted Programs. - Aleksey Nogin (Workshop on Type-Theoretic Languages: Proof Search and Semantics, 2000)

JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. - Stephan Schmitt; Lori Lorigo; Christoph Kreitz; Aleksey Nogin (IJCAR, 2001)

Markov's Principle for Propositional Type Theory. - Alexei Kopylov; Aleksey Nogin (CSL, 2001)

Quotient Types: A Modular Approach. - Aleksey Nogin (TPHOLs, 2002)

Sequent Schema for Derived Rules. - Aleksey Nogin; Jason Hickey (TPHOLs, 2002)

Theory and Implementation of an Efficient Tactic-Based Logical Framework. - Aleksey Nogin (2002)

Compiler implementation in a formal logical framework. - Jason Hickey; Aleksey Nogin; Adam Granicz (MERLIN, 2003)

MetaPRL - A Modular Logical Environment. - Jason Hickey; Aleksey Nogin; Robert L. Constable; Brian E. Aydemir; Eli Barzilay; Yegor Bryukhov; Richard Eaton; Adam Granicz; Alexei Kopylov; Christoph Kreitz; Vladimir Krupski; Lori Lorigo; et al. (TPHOLs, 2003)

A Mechanism for Sequential Consistency in a Distributed Objects System. - Cristian Tapus; Aleksey Nogin; Jason Hickey; Jerome White (PDCS, 2004)

Extensible Hierarchical Tactic Construction in a Logical Framework. - Jason Hickey; Aleksey Nogin (TPHOLs, 2004)

A computational approach to reflective meta-reasoning about languages with bindings. - Aleksey Nogin; Alexei Kopylov; Xin Yu; Jason Hickey (MERLIN, 2005)

: Designing a Scalable Build Process. - Jason Hickey; Aleksey Nogin (FASE, 2006)

Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection. - Jason Hickey; Aleksey Nogin; Xin Yu; Alexei Kopylov (ICFP, 2006)

Practical Reflection for Sequent Logics. - Jason Hickey; Aleksey Nogin; Xin Yu; Alexei Kopylov (LFMTP@FLoC, 2006)

Formalizing Type Operations Using the "Image" Type Constructor. - Aleksey Nogin; Alexei Kopylov (WoLLIC, 2006)

Formal compiler construction in a logical framework. - Jason Hickey; Aleksey Nogin (High. Order Symb. Comput., 2006)

On Dynamic Topological Logic of the Real Line. - Maria Nogin; Aleksey Nogin (J. Log. Comput., 2008)

Programming Time-Multiplexed Reconfigurable Hardware Using a Scalable Neuromorphic Compiler. - Kirill Minkovich; Narayan Srinivasa; Jose M. Cruz-Albrecht; Youngkwan Cho; Aleksey Nogin (IEEE Trans. Neural Networks Learn. Syst., 2012)

HRLSim: A High Performance Spiking Neural Network Simulator for GPGPU Clusters. - Kirill Minkovich; Corey M. Thibeault; Michael John O'Brien; Aleksey Nogin; Youngkwan Cho; Narayan Srinivasa (IEEE Trans. Neural Networks Learn. Syst., 2014)

A verified messaging system. - William Mansky; Andrew W. Appel; Aleksey Nogin (Proc. ACM Program. Lang., 2017)

Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers. - Alexei Kopylov; Stefan Mitsch; Aleksey Nogin; Michael A. Warren (FM, 2021)

Semantics and Axiomatization for Stochastic Differential Dynamic Logic. - Michael Roberts; Alexei Kopylov; Aleksey Nogin (CoRR, 2021)

Assured Point Cloud Perception. - Christopher R. Serrano; Aleksey Nogin; Michael A. Warren (ICAA, 2023)