Mark Bickford - RankMe

36 papers A* 2A 1B 7Misc 1Journal 14Unranked 11

Year	Rank	Type	Title / Venue / Authors
2022	J	`jnl`	Formalizing Moessner's theorem and generalizations in Nuprl. J. Log. Algebraic Methods Program. Mark Bickford, Dexter Kozen, Alexandra Silva
2021	B	`conf`	Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. CSL Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
2019	J	`jnl`	Bar Induction is Compatible with Constructive Type Theory. J. ACM Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable
2019	J	`jnl`	Implementing Euclid's straightedge and compass constructions in type theory. Ann. Math. Artif. Intell. Ariel Kellison, Mark Bickford, Robert L. Constable
2018	B	`conf`	A Verified Theorem Prover Backend Supported by a Monotonic Library. LPAR Vincent Rahli, Liron Cohen, Mark Bickford
2018	A*	`conf`	Computability Beyond Church-Turing via Choice Sequences. LICS Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
2018	J	`jnl`	Connectedness of the continuum in intuitionistic mathematics. Math. Log. Q. Mark Bickford
2018	J	`jnl`	Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. CoRR Mark Bickford
2018	J	`jnl`	Validating Brouwer's continuity principle for numbers using named exceptions. Math. Struct. Comput. Sci. Vincent Rahli, Mark Bickford
2017	A*	`conf`	Bar induction: The good, the bad, and the ugly. LICS Vincent Rahli, Mark Bickford, Robert L. Constable
2017	J	`jnl`	EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
2016	B	`conf`	A nominal exploration of intuitionism. CPP Vincent Rahli, Mark Bickford
2015	J	`jnl`	Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
2014	A	`conf`	Developing Correctly Replicated Databases Using Formal Tools. DSN Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
2014	J	`jnl`	Intuitionistic completeness of first-order logic. Ann. Pure Appl. Log. Robert L. Constable, Mark Bickford
2013	B	`conf`	Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. ITP Vincent Rahli, Mark Bickford, Abhishek Anand
2012	B	`conf`	A diversified and correct-by-construction broadcast service. ICNP Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
2012	—	`conf`	ShadowDB: A Replicated Database on a Synthesized Consensus Core. HotDep Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
2011	J	`jnl`	Intuitionistic Completeness of First-Order Logic CoRR Robert L. Constable, Mark Bickford
2011	J	`jnl`	Knowledge-Based Synthesis of Distributed Systems Using Event Structures Log. Methods Comput. Sci. Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2010	—	`conf`	Automated Proof of Authentication Protocols in a Logic of Events. VERIFY@IJCAR Mark Bickford
2009	—	`conf`	Component Specification Using Event Classes. CBSE Mark Bickford
2008	Misc	`conf`	Nysiad: Practical Protocol Transformation to Tolerate Byzantine Failures. NSDI Chi Ho, Robbert van Renesse, Mark Bickford, Danny Dolev
2008	—	`conf`	Unguessable Atoms: A Logical Foundation for Security. VSTTE Mark Bickford
2006	J	`jnl`	Innovations in computational type theory using Nuprl. J. Appl. Log. Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran
2004	B	`conf`	Knowledge-Based Synthesis of Distributed Systems Using Event Structures. LPAR Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2001	—	`conf`	Protocol Switching: Exploiting Meta-Properties. ICDCS Workshops Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001	—	`conf`	Proving Hybrid Protocols Correct. TPHOLs Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
1999	—	`conf`	Predicate Transformers for Infinite-State Automata in NuPRL Type Theory. IWFM Mark Bickford, Jason Hickey
1996	B	`conf`	Formal Specification and Verification of VHDL. FMCAD Mark Bickford, Damir Jamsek
1994	—	`conf`	Composable specifications for asynchronous systems using UNITY. ASYNC Mark Bickford
1992	—	`conf`	Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification. TPCD Mark Bickford, Mandayam K. Srivas
1990	—	`conf`	A Computer-Aided Verification Tool for Finite State Controller Systems. CAV (DIMACS/AMS volume) Mark Bickford, Mandayam K. Srivas
1990	J	`jnl`	Formal Verification of a Pipelined Microprocessor. IEEE Softw. Mandayam K. Srivas, Mark Bickford
1989	—	`conf`	Verification of a Pipelined Microprocessor Using Clio. Hardware Specification, Verification and Synthesis Mark Bickford, Mandayam K. Srivas
1982	J	`jnl`	Propositional & analogical generation of coordinated verbal, visual & musical texts: U. of Wisconsin. SIGART Newsl. Sheldon Klein, David A. Ross, Mark S. Manasse, Johanna Danos, Mark Bickford, Kendall Jensen, Walter A. Burt, Glenn D. Blank, Walter T. Blanks