Part II. What solutions have people explored?

(at least) 70 years of legal informatics

the legal informatics industry is older than most web developers today

an (incomplete) history in rough chronology; holler if we missed something

Formalising Contracts

• The urge to formalize goes back at least as far as Leibniz, that's the early 18th century
• Lee Loevinger's Jurimetrics -- The Next Step Forward, 1948: "apparently, it has never occurred to the professional disciples of the subject that the trouble with law is not the public but the lawyers, that what is needed is not publicity but progress"
• Layman E. Allen in 1956, Symbolic Logic: A Razor-Edged Tool for Drafting and Interpreting Legal Documents
• Computer Science and Law,1980 where every chapter seems to have become the underpin of at least one legaltech startup
• Some Speculation About Aritificial Intelligence and Legal Reasoning by Bruce G Buchanan & Thomas E Headrick in 1970
• In the 1980s, the British Nationality Act was encoded in Prolog
• The Role of Common Ontology in Achieving Sharable, Reusable Knowledge Bases by Thomas R Gruber in 1991
• The Artificial Intelligence and Law Journal was founded in 1992
• Isomorphism and legal knowledge based systems by TJM Bench-Capon & F P Coenen in 1992
• Attempto Controlled English is an example of a formal/natural hybrid language which could be a compiler target, and has been under development since 1995
• Executable English
• Nick Szabo, Smart Contracts, 1997
• The Representation of Legal Contracts by Daskalopulu & Sergot, 1997
• Composing Contracts: An Adventure in Financial Engineering, 2000 by Simon Peyton Jones, Jean Marc-Eber, and Julian Seward
• Nick Szabo on A Formal Language for Analysing Contracts, a preliminary draft from 2002
• Semantics of Business Vocabulary and Business Rules is a hybrid formal/natural language for business operation and compliance which could also be a compiler target; the RFP was issued in 2003, and v.1.0 of the formal specification was released in 2008
• The Ricardian Contract, 2004 relates legal language with executable code via parameterization
• The RuleML Initiative has been collaborating with OASIS on Legal XML, Policy RuleML, LegalRuleML, and related efforts since 2004; see Modelling Contracts Using RuleML
• Structured Products and Time Travel, 2004 reviews potential solutions for overcoming the challenges of valuing structured products on past, present, and future dates
• Using the Event Calculus for Tracking the Normative State of Contractsby Andrew D. H. Farrell, Mark J. Sergot, Mathias Sallé, Claudio Bartolini, 2005
• Structuring, Pricing, and Processing Complex Financial Products with MLFi, 2005 described MLFi concepts and appliactions
• ContractLog: An Approach to Rule Based Monitoring and Execution of Service Level Agreements by Adrian Paschke, Martin Bichler, and Jens Dietrich, 2005
• Realization of Natural Language Interfaces Using Lazy Functional Programming by RA Frost, 2006
• Towards a Formal Language for Electronic Contracts, 2007 describes CL
• Abstract Specification of Legal Contracts, Prisacariu & Schneider, 2009
• Challenges in the Specification of Full Contracts , GJ Pace and G Schneider, 2009
• Need for a Common Language for All Securities and Financial Contracts, 2010 by the National Research Council
• A Software Tool for Legal Drafting by Daniel Gorin, Sergio Mera, and Fernando Schapachnik, 2011
• Formal Methods as a Link between Software Code and Legal Rules by Daniel Le Métaye, 2011
• Contract Formalisation and Modular Implementation of Domain-Specific Languages, Tom Hvitved's 2012 PhD Thesis (the first chapter offers a comprehensive survey of prior art in contract formalisation)
• Harry Surden on Computable Contracts, 2012
• Towards a common financial language, 2012 speech by Andrew Haldane, Executive Director (Financial Stability) of the Bank of England, at the SIFMA Building a Global Legal Entity Identifier Framework Symposium
• Abubkr Abdelsadiq at Newcastle published a toolkit for model checking contracts using SPIN / Promela rather than Uppaal, 2013
• Examine the tweets of Richard Susskind, author of Tomorrow's Lawyers, 2013
• The REMU project has supported research at the Department of Computer Science at Chalmers University of Technology and the University of Gothenburg, 2013 – 2017; multiple tools on contract analysishave developed therefrom
• These Are Your Rights: A Natural Language Processing Approach to Automated RDF Licenses Generation by E Cabrio, 2014
• Automated Decision Support for Financial Regulatory/Policy Compliance, using Textual Rulelog, by Benjamin Grosof, Janine Bloomfield, Paul Fodor, Michael Kifer, Issac Grosof, Miguel Calejo, and Terrance Swift, 2014
• Stanford University's Computable Contracts Initiative started in 2015
• Next Generation Contracts by Helena Haapio, 2015
• Contracts as Automaton: The Computational Representation of Financial Agreements, Floyd & Goodenough (first published 2015 then revised in 2017)
• Analysing Normative Contracts by John J. Camilleri, 2015
• Smart Contract Templates by Christopher D. Clack, Vikram A. Bakshi, and Lee Braine, 2016
• Bridging the gap between expectation and reality compares smart vs traditional contracts, by Cheng Lim, TJ Saw, and Calum Sargeant, 2016
• Logic in the Theory and Practice of Lawmaking set out the (then) current state of the art regarding the application of logical tools to the problems of theory and practice of lawmaking, 2016
• DMN: Decision Model and Notation Specification, v1.1 was published in June 2016; FEEL: Friendly Enough Expression Language is based on DMN specification conformance level 3 and written using PEG.js-Javascript Parser Generator
• Joe Dewey's essay on ContractCode, 2016
• Toward Machine-Understandable Contracts, 2016 by Sudhir Agarwal, Kevin Xu, and John Moghtader at Stanford, defines CDL, Contract Definition Language (implemented in Prolog), part of work at the Stanford Computable Contracts initiative
• Codex by Pax is a scripting language for Ethereum, 2016; in concert with Pax Directory
• UCL's Centre for Blockchain Technologies had a 2016 public demo of the R3 Corda "fabric" for shared banking ledgers and new programming language, (CLACK), which may inform R3's work (see slides)
• A Domain-Specific Language for Normative Texts with Timing Constraints by R Gulliksson, 2016
• Stephen Wolfram's blogpost in October 2016 about Computational Law, Symbolic Discourse and the AI Constitution
• 2016 Nobel Prize in Economics awarded to Oliver Hart and Bengt Holmström for their work in Contract Theory; in particular, Hart developed foundations for the theory of incomplete contracts and explored the impossibility of writing contracts that anticipate every potential relevant contingency
• Reasoning about Partial Contracts by Shaun Azzopardi, Gordon J. Pace, and Albert Gatt, 2016
• Contracts and Computation — Formal modelling & analysis for normative natural language by John J. Camilleri, 2017
• Kowalski & Sadri's Logic Production Systems relates two dual models of computation: backward-chaining logic programming, and forward-chaining imperative programming. It is being commercialized in the form of Logical Contracts, 2018

• See also: Many other publications by Gerardo Schneider in association with the COSoDIS project using CL for automatic conflict detection
• GR3C
• ORDL
• LegalRuleML is an OASIS Technical Committee
• W3C POE WG
• Here's a list of financial DSLs
• RightsML
• The Estrella Project attempted to "develop and validate an open, standards-based platform allowing public administrations to develop and deploy comprehensive legal knowledge management solutions"; LKIF, an OWL, came out of it
• Algorithmic Contract Types Unified Standards (ACTUS) breaks down financial instruments into a manageable number of cash flow patterns: so-called Contract Types
• CommonForm
• CommonAccord has some early thinking online
• Guido Governatori has published extensively on defeasible logic
• There is a W3C Working Group on Permissions and Obligations Expression which has published an ODRL Vocabulary and Expression draft standard; this is close to RuleML and LegalRuleML
• ABA Futures and ABA Journal
• VCL is a Visual Contract Language

Formalising Regulations

As the richly interpretable saying goes, "Law is Code" and, conversely, Code is Law (Lessig, 2000). Legislative and regulatory constraints may be modeled using a declarative language. Contracts and execution relations may be automatically produced as satisfactions of constraints. TheOracle Policy Automationis a commercial example of it; though Carl Malamud and Thomas Bruce might argue that this should be done in an open way.

• In 1986, Martin Sergot, F Sadri, R A Kowalski, F Kriwaczek, P Hammond, and H T Cory explored The British Nationality Act as a Logic Program
• Logic Programming for Large Scale Applications in Law by George Robinson, Tom Routen, and Marek Sergot (Adam Wyner), 1987
• The Treatment of Negation in Logic Programs for Representing Legislation by Imperial College's Robert Kowalski in 1989
• Since 1988, the Foundation for Legal Knowledge Based Systems (JURIX) has held annual conferences on legal knowledge and information systems; and since 2007, theJURISIN workshop runs alongside
• Towards Regulatory Compliance: Extracting Rights and Obligations to Align Requirements with Regulations, 2006 Travis D Breaux, Matthew W Vail, Annie I Anton
• LREC2010 Workshop Proceedings in 2010
• Digitising the World's Laws, Claire M. Germain, 2010
• On Rule Extraction from Regulations by AZ Wyner abd W Peters, 2011
• An Empirical Approach to the Semantic Representation of Laws by A Wyner, J Bos, V Basile, and P Quaresma, 2012
• New Breakthroughs in Computational Law, 2013
• CO/COUNSEL has been involved in mapping regulatory scapes since 2015
• Xcential’s LegisPro helps legislators get their words out in XML
• FutureLaw 2013: Computational Law and Contracts
• FutureLaw 2014: Forging an Open Legal Document Ecosystem
• Semantic Analysis Regulations, 2018 investigating legal characteristics of Canadian federal regulations
• The Hammurabi Project hosts its DSL in Wolfram Language (Mathematica); an earlier version developed a DSL called Akkadian
• You've heard of XBRL, now the SEC wants Python; see also FpML
• Coninfirm & Bisnode are working on compliance on the blockchain
• IBM's Bluemix Garage announces blockchain project for KYC compliance
• FormaLex published about formalising the Argentinean Customer Protection Act in 2017
• UBS to launch live Ethereum compliance platform

Modelling Performance

• Monitoring multi-party contracts for e-business by Lai Xu, 2004
• Formal Specification of Web Service Contracts for Automated Contracting and Monitoring by Steffen Lamparter, Stefan Luckner, Sybille Mutschler, 2007
• A Contract Compliance Checker by Ioannis Sfyrakis shows an Event-Condition-Action language called EROP, 2012
• Eris:legal brings compatibility with smart contracts

Formal Verification of Smart Contracts

Formal methods and languages like Agda, Idris, Why3, and CoQ, not to mention specification languages like Z, hold much promise. On the spectrum of software reliability, smart contracts ought to live near-mission-critical or life-critical software – cryptosystems, human-crewed spacecraft, hospital equipment. Today, they’re closer to enterprise web-apps.
See The Atlanticon why formal verification is important.

• The need for formal systems appears to be dawning on r/ethereum:   Can we please never again put 100m in a contract without formal correctness proofs?
• The bug which the “DAO hacker” exploited was not “merely in the DAO itself”
• Ethereum’s Solidity is also experimenting with formal verification
• See this list of languages which compile into the EVM

• Languages:  A Survey of Formal Languages for Contracts from FLACOS 2010
• Digital Assest Modelling Language
• Ivy Smart Contract Language

• Papers include:   
• Formal Verification of Smart Contracts
• Certified Symbolic Management of Financial Multi-party Contracts by Patrick Bahr, Jost Berthold, and Martin Elsman, 2015
• Compositional Specification of Commercial Contracts
• Safer smart contracts through type-driven development by Jack Pettersson and Robert Edström, 2016
• Evaluation of Logic-Based Smart Contracts for Blockchain Systems
• A Short Paper on the formal verification of Smart Contracts, 2016
• A Research Agenda in the Validation and Verification of Smart Contracts by Daniele Magazzeni, Peter McBurney, William Nash, 2017

• Startups include:    Adjoint
• Kadena, with PACT
• Tezos
• Cardano

Academia-Industry Partnerships

• Harvard University's Berkman Kein Centre for Internet & Society
• PlainSite
• Law.MIT.edu takes a social-science approach to examining law:   see Dazza's video
• Stanford University's Computational Law
• Stanford University's CodeX Center for Legal Informatics produces a crop of startups every year
• Stanford University's Computable Contracts Initiative
• the Legal Informatics Research Network
• Law OS, a research program on complexity and the law at the Santa Fe Institute
• The Law Lab is an interdisciplinary teaching and research centre set up by Illinois Tech and the Chicago-Kent College of law, and focused on legal innovation technology
• Lexifi's MLFi was one of the earliest commercializations of financial contract formalisation
• CommonAccord
• University of San Diego's Centre for Computation, Mathematics, and the Law
• The Accord Project which was created by legal tech startup Clause and collaborates with the International Association for Contract Management, Hyperledger, Clio, etc.
• University of Swansea has a Centre for Innovation and Entrepreneurship in Law
• University of Oslo has the Norwegian Research Center for Computers and Law
• Osgoode Hall Law School at Toronto's York University is preparing its students to compete against AI

Workshops & Conferences

• The biennial International Conferences on AI & Law (ICAIL) started in 1987
• Since 1988, the Foundation for Legal Knowledge Based Systems (JURIX) has held annual conferences on legal knowledge and information systems JURIX; and since 2007, the JURISIN workshop runs alongside
• LREC2010 Workshop Proceedings in 2010
• The Stanford Centre for Legal Informatics has been running theCodeX FutureLaw Conference since 2013
• AI4J (Artificial Intelligence for Justice), 2016
• The Hacking.Law series of conferences
• 2017 saw the inaugural Legal Geek Conferencein London
• MIT Legal Forum
• Singapore and its inaugural TechLaw.Fest in 2018

• Some are more lawfirm-driven than others:
• ILTACON
• ABA TechShow
• Clio Cloud Conference
• Lawyernomics
• the Law Society of Scotland's Law and technology conference
• LegalWeek in the US