Knowledge Base of
Publications, Seminars, & Math Library

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