Back
  1. Home
  2. Profile of Vincent RAHLI (Unilu)
Profil

RAHLI Vincent

Main Referenced Co-authors
Bickford, Mark (15)
Kamareddine, Fairouz (9)
Constable, Robert L. (7)
Wells, J. B. (6)
Anand, Abhishek (5)
Main Referenced Keywords
Byzantine faults (1); Coq (1); formal verification (1); Information-flow (1); microkernels (1);
Main Referenced Unit & Research Centers
SnT – Interdisciplinary Centre for Security, Reliability and Trust (1)
Main Referenced Disciplines
Computer science (36)

Publications (total 36)

The most downloaded
1169 downloads
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. https://hdl.handle.net/10993/40472

The most cited

43 citations (Scopus®)

Bohrer, B., Rahli, V., Vukotic, I., Volp, M., & Platzer, A. (2017). Formally Verified Differential Dynamic Logic. In CPP 2017. doi:10.1145/3018610.3018616 https://hdl.handle.net/10993/29216

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.
Peer reviewed

Rahli, V., Vukotic, I., Volp, M., & Verissimo, P. (2018). Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In ESOP 2018.
Peer reviewed

Bickford, M., Cohen, L., Constable, R., & Rahli, V. (2018). Computability Beyond Church-Turing via Choice Sequences. In LICS 2018.
Peer reviewed

Rahli, V., Cohen, L., & Bickford, M. (2018). A Verified Theorem Prover Backend Supported by a Monotonic Library. In LPAR 2018.
Peer reviewed

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.

Bohrer, B., Rahli, V., Vukotic, I., Volp, M., & Platzer, A. (2017). Formally Verified Differential Dynamic Logic. In CPP 2017. doi:10.1145/3018610.3018616
Peer reviewed

Rahli, V., & Bickford, M. (2017). Validating Brouwer's Continuity Principle for Numbers Using Named Exceptions. Mathematical Structures in Computer Science. doi:10.1017/S0960129517000172
Peer reviewed

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
Peer reviewed

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
Peer Reviewed verified by ORBi

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. (2016). Exercising Nuprl's Open-Endedness. In The 5th International Congress on Mathematical Software.

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
Peer reviewed

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
Peer reviewed

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).

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
Peer reviewed

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
Peer reviewed

Anand, A., & Rahli, V. (2014). Towards a Formally Verified Proof Assistant (technical report). Cornell University.

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
Peer reviewed

Anand, A., Bickford, M., Constable, R. L., & Rahli, V. (2014). A Type Theory with Partial Equivalence Relations as Types [Paper presentation]. TYPES 2014.

Anand, A., & Rahli, V. (2014). A Generic Approach to Proofs about Substitution. In LFMTP 2014. doi:10.1145/2631172.2631177
Peer reviewed

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.
Peer reviewed

Rahli, V., Bickford, M., & Anand, A. (2013). Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. In ITP 2013.
Peer reviewed

Bickford, M., Constable, R. L., Eaton, R., Guaspari, D., & Rahli, V. (2012). Introduction to EventML.

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
Peer reviewed

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.
Peer reviewed

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., 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
Peer reviewed

Kamareddine, F., Rahli, V., & Wells, J. B. (2012). Reducibility proofs in the lambda-calculus. Fundamenta Informaticae, 121. doi:10.3233/FI-2012-773
Peer reviewed

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.

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
Peer reviewed

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).

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). A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables. In ICTAC 2008.
Peer reviewed

Mogbil, V., & Rahli, V. (2007). Uniform Circuits & Boolean Proof Nets. In LFCS 2007. doi:10.1007/978-3-540-72734-7_28
Peer reviewed

Contact ORBilu