![]() ![]() | VUKOTIC, I., RAHLI, V., & VERISSIMO, P. (2019). Asphalion: Trustworthy Shielding Against Byzantine Faults. In I. VUKOTIC, V. Rahli, ... P. VERISSIMO, Asphalion: Trustworthy Shielding Against Byzantine Faults. ![]() |
![]() ![]() | RAHLI, V., VUKOTIC, I., VOLP, M., & VERISSIMO, P. (2018). Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In ESOP 2018. ![]() |
![]() ![]() | RAHLI, V., Cohen, L., & Bickford, M. (2018). A Verified Theorem Prover Backend Supported by a Monotonic Library. In LPAR 2018. ![]() |
![]() ![]() | Mirto, C., Yu, J., RAHLI, V., & VERISSIMO, P. (2018). Probabilistic Formal Methods Applied to Blockchain’s Consensus Protocol [Paper presentation]. DSN Workshop on Byzantine Consensus and Resilient Blockchains. |
![]() ![]() | Bickford, M., Cohen, L., Constable, R., & RAHLI, V. (2018). Computability Beyond Church-Turing via Choice Sequences. In LICS 2018. ![]() |
![]() ![]() | RAHLI, V., Bickford, M., & Constable, R. (2017). Bar Induction: The Good, the Bad, and the Ugly. In Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). doi:10.1109/LICS.2017.8005074 ![]() |
![]() ![]() | RAHLI, V., & Bickford, M. (2017). Validating Brouwer's Continuity Principle for Numbers Using Named Exceptions. Mathematical Structures in Computer Science. doi:10.1017/S0960129517000172 ![]() |
![]() ![]() | RAHLI, V., Guaspari, D., Bickford, M., & Constable, R. (2017). EventML: Specification, Verification, and Implementation of Crash-Tolerant State Machine Replication Systems. Science of Computer Programming. doi:10.1016/j.scico.2017.05.009 ![]() |
![]() ![]() | Bohrer, B., RAHLI, V., VUKOTIC, I., VOLP, M., & Platzer, A. (2017). Formally Verified Differential Dynamic Logic. In CPP 2017. doi:10.1145/3018610.3018616 ![]() |
![]() ![]() | VOLP, M., Lackorzynski, A., DECOUCHANT, J., RAHLI, V., ROCHA, F., & VERISSIMO, P. (12 December 2016). Avoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control [Paper presentation]. 1st Workshop on System Software for Trusted Execution (SysTEX '16), Trento, Italy. doi:10.1145/3007788.3007794 |
![]() ![]() | RAHLI, V., Wells, J., Pirie, J., & Kamareddine, F. (2016). Skalpel: A Constraint-Based Type Error Slicer for Standard ML. Journal of Symbolic Computation. doi:10.1016/j.entcs.2015.04.012 ![]() |
![]() ![]() | RAHLI, V. (2016). Exercising Nuprl's Open-Endedness. In The 5th International Congress on Mathematical Software. |
![]() ![]() | RAHLI, V., & Bickford, M. (2016). A Nominal Exploration of Intuitionism. In The 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016). doi:10.1145/2854065.2854077 ![]() |
![]() ![]() | RAHLI, V., Wells, J. B., Pirie, J., & Kamareddine, F. (2015). Skalpel: A Type Error Slicer for Standard ML. Electronic Notes in Theoretical Computer Science. doi:10.1016/j.entcs.2015.04.012 ![]() |
![]() ![]() | RAHLI, V., Guaspari, D., Bickford, M., & Constable, R. L. (2015). Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. EASST. doi:10.14279/tuj.eceasst.72.1013.1007 ![]() |
![]() ![]() | RAHLI, V., & Bickford, M. (2015). Coq as a Metatheory for Nuprl with Bar Induction [Paper presentation]. Continuity, Computability, Constructivity – From Logic to Algorithms (CCC 2015). |
![]() ![]() | Anand, A., & RAHLI, V. (2014). Towards a Formally Verified Proof Assistant (technical report). Cornell University. https://orbilu.uni.lu/handle/10993/22652 |
![]() ![]() | Anand, A., & RAHLI, V. (2014). A Generic Approach to Proofs about Substitution. In LFMTP 2014. doi:10.1145/2631172.2631177 ![]() |
![]() ![]() | Anand, A., Bickford, M., Constable, R. L., & RAHLI, V. (2014). A Type Theory with Partial Equivalence Relations as Types [Paper presentation]. TYPES 2014. |
![]() ![]() | Schiper, N., RAHLI, V., Van Renesse, R., Bickford, M., & Constable, R. L. (2014). Developing Correctly Replicated Databases Using Formal Tools. In DSN 2014. doi:10.1109/DSN.2014.45 ![]() |
![]() ![]() | Anand, A., & RAHLI, V. (2014). Towards a Formally Verified Proof Assistant. In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. ![]() |
![]() ![]() | RAHLI, V., Bickford, M., & Anand, A. (2013). Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. In ITP 2013. ![]() |
![]() ![]() | Bickford, M., Constable, R. L., Eaton, R., Guaspari, D., & RAHLI, V. (2012). Introduction to EventML. https://orbilu.uni.lu/handle/10993/22683 |
![]() ![]() | RAHLI, V. (2012). Interfacing with Proof Assistants for Domain Specific Programming Using EventML [Paper presentation]. International Workshop on User Interfaces for Theorem Provers (UITP 2012). |
![]() ![]() | RAHLI, V., Schiper, N., Renesse, R. V., Bickford, M., & Constable, R. L. (2012). A diversified and correct-by-construction broadcast service. In ICNP 2012. doi:10.1109/ICNP.2012.6459943 ![]() |
![]() ![]() | Schiper, N., RAHLI, V., Renesse, R. V., Bickford, M., & Constable, R. L. (2012). ShadowDB: A Replicated Database on a Synthesized Consensus Core. In HotDep 2012. ![]() |
![]() ![]() | Bickford, M., Constable, R. L., & RAHLI, V. (2012). Logic of Events, a framework to reason about distributed systems [Paper presentation]. Languages for Distributed Algorithms Workshop (LADA 2012). |
![]() ![]() | Kamareddine, F., RAHLI, V., & Wells, J. B. (2012). Reducibility proofs in the lambda-calculus. Fundamenta Informaticae, 121. doi:10.3233/FI-2012-773 ![]() |
![]() ![]() | Kamareddine, F., Nour, K., RAHLI, V., & Wells, J. B. (2012). On Realisability Semantics for Intersection Types with Expansion Variables. Fundamenta Informaticae, 121. doi:10.3233/FI-2012-774 ![]() |
![]() ![]() | RAHLI, V. (2011). Investigations in intersection types: Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method [Doctoral thesis, Heriot-Watt University]. ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/22668 |
![]() ![]() | RAHLI, V., Wells, J. B., & Kamareddine, F. (2010). A constraint system for a SML type error slicer. (HW-MACS-TR-0079). Heriot-Watt University, MACS, ULTRA group. https://orbilu.uni.lu/handle/10993/22673 |
![]() ![]() | Kamareddine, F., & RAHLI, V. (2009). Simplified Reducibility Proofs of Church-Rosser for beta- and beta-eta-reduction. Electronic Notes in Theoretical Computer Science, 247, 85--101. doi:10.1016/j.entcs.2009.07.050 ![]() |
![]() ![]() | Kamareddine, F., Nour, K., RAHLI, V., & Wells, J. B. (2008). A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables. In ICTAC 2008. ![]() |
![]() ![]() | Kamareddine, F., RAHLI, V., & Wells, J. B. (2008). Reducibility Proofs in the λ-Calculi with Intersection Types [Paper presentation]. Workshop on Intersection Types and Related Systems (ITRS 2008). |
![]() ![]() | Kamareddine, F., Nour, K., RAHLI, V., & Wells, J. B. (2008). Realisability Semantics for Intersection Types and Expansion Variables [Paper presentation]. Workshop on Intersection Types and Related Systems (ITRS 2008). |
![]() ![]() | Mogbil, V., & RAHLI, V. (2007). Uniform Circuits & Boolean Proof Nets. In LFCS 2007. doi:10.1007/978-3-540-72734-7_28 ![]() |