nectry research / publications

Foundational Research.

Nectry's technology is built on two decades of research at MIT in programming languages, formal methods, and security. The papers below are the primary sources behind what the product does.

§ 1

The research that powers Nectry.

—
Security policies are mathematically verified before deployment, ensuring enterprise-grade guarantees.[4]
—
A unified programming model spans client, server, and database, enabling whole-program optimization.[3]
—
Optimizing compiler technology produces efficient code from high-level specifications.[2]
—
A powerful type system supporting metaprogramming guarantees that generated programs contain no invalid code.[1]
—
Access control is enforced at the database level, with zero runtime overhead.[4]
—
Information flow is tracked to prevent data leaks.[4]
§ 2

Publications.

[1]
Ur: Statically-Typed Metaprogramming with Type-Level Record Computation
Adam Chlipala/PLDI '10

Presents Ur, a language that uses functional programs as specifications to safely support metaprogramming, and demonstrates the approach through Ur/Web, a web-development framework that ensures type-safe code generation without requiring explicit proofs or complex types from the user.

Download PDF
[2]
An Optimizing Compiler for a Purely Functional Web-Application Language
Adam Chlipala/ICFP '15

Describes a compiler that transforms high-level functional programs into efficient code, showing that purely functional languages can match imperative languages in performance for real-world web applications.

Download PDF
[3]
Ur/Web: A Simple Model for Programming the Web
Adam Chlipala/POPL '15

Introduces a unified programming model for web applications that spans client, server, and database tiers, enabling whole-program reasoning and optimization while maintaining simplicity.

Download PDF
[4]
Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications
Adam Chlipala/OSDI '10

Demonstrates how to statically verify security policies that vary based on database contents, using symbolic evaluation and automated theorem-proving to guarantee security properties without runtime overhead.

Download PDF