Formally verified differential dynamic logic R Bohrer, V Rahli, I Vukotic, M Völp, A Platzer Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 78 | 2017 |

Velisarios: Byzantine fault-tolerant protocols powered by Coq V Rahli, I Vukotic, M Völp, P Esteves-Verissimo Programming Languages and Systems: 27th European Symposium on Programming …, 2018 | 57 | 2018 |

Towards a formally verified proof assistant A Anand, V Rahli Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 53 | 2014 |

Developing correctly replicated databases using formal tools N Schiper, V Rahli, R Van Renesse, M Bickford, RL Constable 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems …, 2014 | 46 | 2014 |

DAMYSUS: streamlined BFT consensus leveraging trusted components J Decouchant, D Kozhaya, V Rahli, J Yu Proceedings of the Seventeenth European Conference on Computer Systems, 1-16, 2022 | 43 | 2022 |

Formal specification, verification, and implementation of fault-tolerant systems using EventML V Rahli, D Guaspari, M Bickford, R Constable Electronic Communications of the EASST 72, 2015 | 40 | 2015 |

A nominal exploration of intuitionism V Rahli, M Bickford Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 32 | 2016 |

The Logic of Events, a framework to reason about distributed systems M Bickford, R Constable, V Rahli 2012 Languages for Distributed Algorithms (LADA) workshop, 2012 | 24 | 2012 |

Practical Byzantine reliable broadcast on partially connected networks S Bonomi, J Decouchant, G Farina, V Rahli, S Tixeuil 2021 IEEE 41st International Conference on Distributed Computing Systems …, 2021 | 22 | 2021 |

Skalpel: A type error slicer for standard ML V Rahli, J Wells, J Pirie, F Kamareddine Electronic Notes in Theoretical Computer Science 312, 197-213, 2015 | 21 | 2015 |

Pistis: an event-triggered real-time byzantine-resilient protocol suite D Kozhaya, J Decouchant, V Rahli, P Esteves-Verissimo IEEE Transactions on Parallel and Distributed Systems 32 (9), 2277-2290, 2021 | 20 | 2021 |

Formal Program Optimization in *Nuprl* Using Computational Equivalence and Partial TypesV Rahli, M Bickford, A Anand Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 20 | 2013 |

EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems V Rahli, D Guaspari, M Bickford, RL Constable Science of Computer Programming 148, 26-48, 2017 | 19 | 2017 |

A constraint system for a SML type error slicer V Rahli, JB Wells, F Kamareddine Heriot-Watt University, MACS, ULTRA group, 2010 | 19 | 2010 |

Validating Brouwer's continuity principle for numbers using named exceptions V Rahli, M Bickford Mathematical Structures in Computer Science 28 (6), 942-990, 2018 | 16 | 2018 |

Interfacing with proof assistants for domain specific programming using EventML V Rahli International Workshop on User Interfaces for Theorem Provers (UITP 2012), 2012 | 16 | 2012 |

Computability beyond church-turing via choice sequences M Bickford, L Cohen, RL Constable, V Rahli Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 14 | 2018 |

Uniform circuits, & boolean proof nets V Mogbil, V Rahli International Symposium on Logical Foundations of Computer Science, 401-421, 2007 | 13 | 2007 |

A type theory with partial equivalence relations as types A Anand, M Bickford, RL Constable, V Rahli | 12 | 2014 |

Bar induction: The good, the bad, and the ugly V Rahli, M Bickford, RL Constable 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017 | 10 | 2017 |