Skip to main content
PRL Project

Knowledge Base of
Publication Publications, Seminar Seminars, & Math Book Math Library

PhD theses from the project are accessible at the NCSTRL web site.

Browse by author | title | year | subject

Filter for: Vincent Rahli

29 results


Publication Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020

Publication Bar Induction is Compatible with Constructive Type Theory | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019

Publication A Verified Theorem Prover Backend Supported by a Monotonic Library | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford
November 01, 2018

Publication Validating Brouwer’s Continuity Principle for Numbers Using Named Exceptions | cite »
by Vincent Rahli, Mark Bickford
January 02, 2018

Publication Computability Beyond Church-Turing using Choice Sequences | cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018

Publication EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems | cite »
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
November 15, 2017

Publication Bar Induction: The Good, the Bad, and the Ugly | cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017

Publication A Nominal Exploration of Intuitionism
by Vincent Rahli, Mark Bickford
January 18, 2016

Publication Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
September 14, 2015

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015

Publication Nuprl’s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015

Seminar Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014

Seminar There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014

Seminar A Type Theory with Partial Equivalence Relations as Types
by Vincent Rahli
September 10, 2014

Publication A Generic Approach to Proofs about Substitution
by Abhishek Anand, Vincent Rahli
July 17, 2014

Publication Towards a Formally Verified Proof Assistant
by Abhishek Anand, Vincent Rahli
July 14, 2014

Publication Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Publication A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014

Seminar How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013

Seminar A verified proof assistant
by Vincent Rahli, Abhishek Anand
October 30, 2013

Publication Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types | cite »
by Vincent Rahli, Mark Bickford, Abhishek Anand
April 22, 2013

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013

Publication A Diversified and Correct-by-Construction Broadcast Service | cite »
by Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 30, 2012

Publication ShadowDB: A Replicated Database on a Synthesized Consensus Core | cite »
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 07, 2012

Publication Interfacing with Proof Assistants for Domain Specific Programming Using EventML | cite »
by Vincent Rahli
July 11, 2012

Publication The Logic of Events, a framework to reason about distributed systems | cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Publication Introduction to Classic ML | cite »
by Christoph Kreitz, Vincent Rahli
2011

Publication Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method | cite »
by Vincent Rahli
2011