Quipper: a scalable quantum programming language AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron ACM SIGPLAN Notices 48 (6), 333-342, 2013 | 206 | 2013 |

The simplicial model of univalent foundations (after Voevodsky) C Kapulkin, PLF Lumsdaine arXiv preprint arXiv:1211.2851, 2012 | 187 | 2012 |

Weak omega-categories from intensional type theory PLF Lumsdaine | 107 | 2008 |

Semantics of higher inductive types PLF Lumsdaine, M Shulman Mathematical Proceedings of the Cambridge Philosophical Society, 1-50, 2017 | 56* | 2017 |

An introduction to quantum programming in quipper AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron International Conference on Reversible Computation, 110-124, 2013 | 52 | 2013 |

The local universes model: an overlooked coherence construction for dependent type theories PLF Lumsdaine, MA Warren ACM Transactions on Computational Logic (TOCL) 16 (3), 23, 2015 | 51* | 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 | 43 | 2017 |

Homotopy limits in Coq J Avigad, K Kapulkin, PLF Lumsdaine arXiv preprint arXiv:1304.0680, 4, 2013 | 31* | 2013 |

Higher inductive types: a tour of the menagerie PLF Lumsdaine URl: http://homotopytypetheory. org/2011/04/24/higher-induc tive-types-a …, 2011 | 21 | 2011 |

Univalence in simplicial sets C Kapulkin, PLF Lumsdaine, V Voevodsky arXiv preprint arXiv:1203.2553, 2012 | 18 | 2012 |

Higher Categories from Type Theories (CT2011, Vancouver) PLF Lumsdaine | 16* | 2010 |

Model structures from higher inductive types PL Lumsdaine Unpublished note, December, 2011 | 12 | 2011 |

The homotopy theory of type theories K Kapulkin, PLF Lumsdaine Advances in Mathematics 337, 1-38, 2018 | 7 | 2018 |

Categorical structures for type theory in univalent foundations B Ahrens, PLF Lumsdaine, V Voevodsky arXiv preprint arXiv:1705.04310, 2017 | 7 | 2017 |

A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory KB Hou, E Finster, D Licata, PLF Lumsdaine arXiv preprint arXiv:1605.03227, 2016 | 7* | 2016 |

Lawvere–Tierney sheaves in algebraic set theory S Awodey, N Gambino, PL Lumsdaine, MA Warren The Journal of Symbolic Logic 74 (3), 861-890, 2009 | 7 | 2009 |

Displayed Categories B Ahrens, PLF Lumsdaine arXiv preprint arXiv:1705.04296, 2017 | 5 | 2017 |

Parametricity, automorphisms of the universe, and excluded middle AB Booij, MH Escardó, PLF Lumsdaine, M Shulman arXiv preprint arXiv:1701.05617, 2017 | 4 | 2017 |

On the Bourbaki–Witt principle in toposes A Bauer, PL Lumsdaine Mathematical Proceedings of the Cambridge Philosophical Society 155 (1), 87-99, 2013 | 4 | 2013 |

A Coq proof that Univalence Axioms implies Functional Extensionality A Bauer, PLF Lumsdaine | 3 | 2011 |