Kenneth Knowles

Engineer, Computer Scientist, Collaborator



2014 - present


Software Engineer



Lead Engineer

Responsible for software development outcomes, from strategy to execution and subsequent analysis. Leading a hand-picked team of three senior engineers as well as overseeing engagements with usability analysts, designers, overseas resources, etc. ArborBridge delivers personalized educational services using proprietary curricula developed according to advances in technology, pedagogy, and neuroscience.



Senior Engineer

Led development of REST API and export tools for CommCare users to extract and transform their data. Contributed broadly to CommCare's backend design and implementation, including improvements to continuous integration, continuous deployment, asynchronous ETL processes, and modern role-based access control. Also started the Dimagi band :-)

2010 - 2012


Platform Engineer

Instrumental in building the Inkling platform, including REST APIs, web store, publishing tools, distributed build processes, and automated deployment. Directed improvements to Inkling's search capabilities. Directed analytics projects, coordinating business analysts, designers, front-end and back-end developers.

2009 - 2010


iPhone Application Engineer

Developed iPhone apps for Fortune 500 brands including Gap, Timberline, Target and Cooks Illustrated, regularly featured in Apple commercials and stores.

2004 - 2009

University of California - Santa Cruz

Research and Teaching Assistant

Developed hybrid type systems, which blend compile-time guarantees with run-time checks, proven to detect all type errors in an undecidable type system either statically or dynamically, and to catch more errors statically than a conventional type system. Proved that type inference for such type systems in decidable even though type checking is not. Delivered supplementary lectures and led seminars in graduate-level Computer Science courses. See also selected publications below.

2000 - 2004

Cityspan Technologies

Senior Programmer

Led the development team building Cityspan's principle product,, an information management system now used by over 100 large not-for-profit clients such as the Chicago Public Schools. Conceived and created a language for nontechnical personnel to customize the product, an early AJAX-accelerated user interface, and a query and reporting system.

2003 - 2004

University of California - Berkeley

Research Assistant

Under professor Brian Harvey, added object-oriented features to the UC Berkeley Logo implementation. Under research director Adrian Freed of the Center for New Music and Audio Technologies, prototyped a C++/OpenGL interface for the Open Sound World visual programming language. Under graduate student researcher Ravi Kolluri, implemented and benchmarked heuristic optimizations to algorithms for reconstruction of solid models from 3-D laser scanner data.


University of California - Santa Cruz

Doctor of Philosophy - Computer Science

Doctoral dissertation: Executable Refinement Types. See also selected publications below.

University of California - Santa Cruz

Master of Science - Computer Science

Master's thesis: Hybrid Type Checking and Type Reconstruction for Executable Refinement Types. See also selected publications below. Founded UCSC's weekly programing language reading group for classic papers and ongoing research. Co-founded The "What Is ... ?" Graduate Seminar (TWIGS) at UCSC, a voluntary cross-disciplinary seminar on math and science topics. Four-time recipient of the UC Regents' Fellowship.

University of Oregon

Graduate summer schools on programming languages

2008 Summer School on Logic and Theorem Proving in Programming Languages.
2007 Summer School on Language-Based Techniques for Integrating with the External World.
2006 Summer School on Language-Based Techiques for Concurrent and Distributed Systems.

University of California - Berkeley

Bachelor of Science - Electrical Engineering and Computer Science

Recipient of the National Merit Scholarship. Performed undergraduate research in computational geometry, computer music, and object-oriented programming languages.

Selected Publications

Faceted Dynamic Information Flow via Control and Data Monads (pdf)

With Thomas Schmitz, Duston Rhodes, Thomas H. Austin, and Cormac Flanagan. In Principles of Security and Trust, 2016 (POST'16).

Hybrid Type Checking. (pdf)

With Cormac Flanagan. In Transaction on Programming Languages and Systems, 2010 (TOPLAS'10).

Compositional and Decidable Checking for Dependent Contract Types. (pdf)

With Cormac Flanagan. In Proceedings of Programming Languages meets Program Verification, 2009 (PLPV'09).

Proving correctness of a dynamic atomicity analysis in Coq. (abstract)

With Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan. In Proceedings of the Workshop on Mechanizing Metatheory, 2008 (WMM'08).

First-Order Logic A la Carte. (pdf)

In The Monad Reader Issue 11, 2008.

Type Reconstruction for General Refinement Types. (pdf) (extended)

With Cormac Flanagan. In Proceedings of the European Symposium on Programming, 2007 (ESOP'07).

Sage: Hybrid Checking for Expressive Specifications. (pdf) (extended) (site)

With Jessica Gronski, Aaron Tomb, Cormac Flanagan, and Stephen Freund. In Proceedings of the Workshop on Scheme and Functional Programming, 2006 (SFP'06).


Spring 2007

Parallel SAT Algorithm Comparison

Experimentally compared parallelization strategies for boolean 3-SAT using advanced constructs available in the Haskell programming language. (For a Ph.D. course in parallel programming techniques at UC Santa Cruz)

Spring 2005

Row Type Inference

Implemented row-polymorphic type reconstruction for a lambda calculus with row types for extensible records and variants (For a Ph.D. course in type systems at UC Santa Cruz)

Spring 2005

Failure Detector Comparison

Wrote a multithreaded network simulator in Objective Caml and compared various algorithms for failure detection in distributed systems. (For a master-level course in distributed systems at UC Santa Cruz)

Fall 2004

Senate Vote Prediction

Applied machine learning algorithms to the problem of predicting senators’ votes on a new bill, using a feature set drawn from the text of senate bills, and the senators’ past votes. (For a master-level course in machine learning at UC Santa Cruz)

Spring 2003

Markov Chain Music

Experimented with generation of music using Markov chains and higher-order functions in Objective Caml. (For a Ph.D. seminar in computer music at UC Berkeley)

Fall 2003

Survey of Set-Based Analysis

Presented a survey of set-based analysis for a an audience in computer science, but not necessarily expert in programming languages. (For a master-level course in programming languages at UC Berkeley)

Fall 2002

Survey of Proof-Carrying Code

Presented a survey of proof-carrying code research for an audience of scientists, but not necessarily computer scientists. (For an undergraduate technical writing course at UC Berkeley)



Languages Libraries &
Other Tech 3rd Party
Services & APIs
Shipped or
published using...
  • Python
  • Scala
  • Java
  • Objective C
  • Haskell
  • Puppet
  • OCaml
  • Javascript
  • Compass/Sass
  • C
  • SQL
  • Coq
  • C#
  • Tornado
  • Django
  • Cocoa
  • Thrift
  • d3.js
  • Leaflet.js
  • Knockout.js
  • Backbone.js
  • jQuery
  • MySQL
  • PostgreSQL
  • Cassandra
  • MongoDB
  • Redis
  • Memcache
  • RabbitMQ
  • ElasticSearch
  • Apache
  • Amazon S3
  • Cloudfront
  • Facebook
  • Shopstyle
  • Basecamp
  • Birst
Built large
projects using...
  • PHP
  • C++
  • Matlab/Scilab/Octave
  • OpenGL
  • GLUI
Experienced with...
  • Perl
  • Ruby
  • Pascal
  • Isabelle/HOL
  • Sencha/ExtJS
  • FBConnect
Contributed bits to... ElasticSearch, pfff, PLY, Scalaz Tastypie Roy CommCareHQ CouchdbKit Radon Claire
Originated... CommCare Export, O'Caml FreeTDS, puppet-postgresql, Scala-RelaxNG, JSONPath-RW,

Misc Interests


Co-created, arranged, performed, and produced five studio albums. Co-arranged, produced, and conducted synthesized accompaniment to community West Side Story production. Co-created, arranged, promoted, and ran all-day, two-stage music festival.


Co-founder of UC Santa Cruz Chess and Go Players. Rated 5 kyu by Nihon Ki-in.