#
Knowledge Base of

Publications,
Seminars,
& Math Library

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

## Filter for: Vincent Rahli

29 results

*
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic *

by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen

2020

*
Bar Induction is Compatible with Constructive Type Theory *
| cite »

by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable

2019

*
A Verified Theorem Prover Backend Supported by a Monotonic Library *
| cite »

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

*
Validating Brouwerâ€™s Continuity Principle for Numbers Using Named Exceptions *
| cite »

by Vincent Rahli, Mark Bickford

January 02, 2018

*
Computability Beyond Church-Turing using Choice Sequences *
| cite »

by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable

2018

*
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

*
Bar Induction: The Good, the Bad, and the Ugly *
| cite »

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 2015

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Nuprlâ€™s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
Nominal Type Theory *

by Mark Bickford, Vincent Rahli

October 29, 2014

*
There Are No Discontinuous Real Functions *

by Mark Bickford, Vincent Rahli

October 08, 2014

*
A Type Theory with Partial Equivalence Relations as Types *

by Vincent Rahli

September 10, 2014

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 2014

*
Developing Correctly Replicated Databases Using Formal Tools *

by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

June 23, 2014

*
A Type Theory with Partial Equivalence Relations as Types *

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

May 12, 2014

*
How far can we go with Induction-Recursion? *

by Abhishek Anand, Vincent Rahli

November 20, 2013

*
A verified proof assistant *

by Vincent Rahli, Abhishek Anand

October 30, 2013

*
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types *
| cite »

by Vincent Rahli, Mark Bickford, Abhishek Anand

April 22, 2013

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

March 31, 2013

*
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

*
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

*
Interfacing with Proof Assistants for Domain Specific Programming Using EventML *
| cite »

by Vincent Rahli

July 11, 2012

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

2012

*
Simple Consensus Algorithm *

by Robert L. Constable, Mark Bickford, Vincent Rahli

October 28, 2011

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

*
Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method *
| cite »

by Vincent Rahli

2011