Ryan Wisnesky

Curriculum Vitae
Email | Twitter

Ryan Wisnesky obtained B.S. and M.S. degrees in mathematics and computer science from Stanford University and a Ph.D. in computer science from Harvard University, where he studied the design and implementation of provably correct software systems. While at IBM Research Almaden he contributed to the Clio, Orchid, and HIL projects. While a postdoctoral associate in the MIT department of mathematics, he developed the CQL query language based on category theory. He currently leads open-source and commercial development of CQL as CTO of Conexus AI.

Current Activities

Project Elway seeks to replace legacy government and enterprise software applications with more sophisticated, next-generation mathematical components built on Kan extensions using CQL. As they "rejoice in light and give it back in hues more marvellous than before", the Silmarils reflect the universally generative nature of Kan extensions, and even in the darkness of the smallest data sets Kan extensions "of their own radiance shine like the stars".

Consensus-Free Spreadsheet Integration (Draft, 2022)
Algebraic Property Graphs (Draft, 2022). See also Hydra
Fast Left Kan Extensions Using the Chase (JAR 2022)
Informal Data Transformation Considered Harmful (HAI 2019)
Categorical Data Integration for Computational Science (CMS 2019)

Previous Activities

	I developed CQL first at Harvard and MIT and then at Conexus AI. Algebraic Databases (TAC 2017) [slides] [video] Algebraic Data Integration (JFP 2017) [Aggregation supplement] Using Category Theory to Facilitate Multiple Manufacturing Service Database Integration (JCISE 2017) Algebraic Model Management (WADT 2016) QINL: Query-Integrated Languages (2015) Relational Foundations for Functorial Data Migration (DBPL 2015) [slides]
	I developed next-generation functional query languages and explored their application to no-sql. Using Dependent Types to Semantically Optimize Language-Integrated Queries (DBPL 2015) [slides] Functional Query Languages with Categorical Types (Dissertation 2014) [slides] [Coq] [Code] [Addendum] Collection Processing with Constraints, Monads, and Folds (WIR 2011) [slides] Minimizing Monad Comprehensions (Tech Report 2011)
	I've built certified systems software with Ynot, and started the Coq formalization of Hashgraph (later continued by Gregory Malecha and finished by Karl Krary). Trace Based Verification of Imperative Programs with I/O (JSC-WWV 2010) Toward a Verified Relational Database Management System (POPL 2010) [Slides] Effective Interactive Proof of Higher Order Imperative Programs (ICFP 2009) Certified Web Services in Ynot (WWV 2009) [Slides]
	I've developed programming languages for relational data integration. High-Level Rules for Integration and Analysis of Data: New Challenges (PBF 2013) HIL: A High-Level Scripting Language for Entity Integration (EDBT 2013) Mapping Polymorphism (ICDT 2010) [Proofs] [Slides] Mapping Dependence (Tech Report 2009) Orchid: Integrating Schema Mapping and ETL (ICDE 2008)
	I'm a former IBM Extreme Blue intern. Bringing Business Objects into Extract-Transform-Load Technology (BIMA 2008) Callisto: Mergers without Pain (BIRTE 2006)
	Unpublished reports from MIT. Functorial Data Migration: From Theory to Practice
	Unpublished reports from Harvard. The Inadequacy of Pure Intention Exploring Webgraph Compression with SUBDUE
	Unpublished reports from Stanford. The Inheritance Anomaly Revisited Evaluating Scheduling Algorithms on Distributed Computational Grids