Skip to content

Research at St Andrews

Subtype polymorphism à la carte via machine learning on dependent types

Research output: Chapter in Book/Report/Conference proceedingConference contribution



Jerry Swan, Colin G. Johnson, Edwin C. Brady

School/Research organisations


The essential rationale for subtype polymorphism is adherence to the 'Open/Closed Principle' [12]: the ability to write framework code in terms of superclasses and subsequently invoke it with any subclass that exhibits 'proper subtyping' via the Liskov Substitution Principle (LSP) [11]. Formally, the LSP states that if ø(t : T) is a provable property of objects t of type T, then ø(s) should be true for objects s of subtype S of T. In practice, such properties have typically been those expressible via 'Design by Contract' [12], specifically preconditions, postconditions and invariants. Such abstraction via subtype polymorphism is intended to insulate against requirements change. However, when new requirements do necessitate a change of contract, the maintenance consequences can be severe. In the (typical) absence of explicit language or tool support, enforcement of proper subtyping is laborious and error-prone: contractual changes typically require manual inspection/repair of the class hierarchy to determine/address violations of the LSP.


Original languageEnglish
Title of host publicationCompanion Proceedings for the ISSTA/ECOOP 2018 Workshops
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery, Inc
Number of pages3
ISBN (Electronic)9781450359399
Publication statusPublished - 16 Jul 2018
Event2nd International Workshop on Machine Learning techniques for Programming Languages - Amsterdam, Netherlands
Duration: 18 Jul 201818 Jul 2018
Conference number: 2


Workshop2nd International Workshop on Machine Learning techniques for Programming Languages
Abbreviated titleML4PL
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Value-dependent session design in a dependently typed language

    de Muijnck-Hughes, J., Brady, E. C. & Vanderbauwhede, W., 2 Apr 2019, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, Prague, Czech Republic, 7th April 2019. Martins, F. & Orchard, D. (eds.). Open Publishing Association, p. 47-59 (Electronic Proceedings in Theoretical Computer Science; vol. 291).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Type driven development of concurrent communicating systems

    Brady, E. C., 7 Jul 2017, In : Computer Science. 18, 3, 22 p., 1413.

    Research output: Contribution to journalArticle

  3. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C., 17 Mar 2017, In : Logical Methods in Computer Science. 13, 1, 23 p., 7.

    Research output: Contribution to journalArticle

  4. Type-driven development with Idris

    Brady, E. C., Mar 2017, Shelter Island: Manning Publications Co. 480 p.

    Research output: Book/ReportBook

  5. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C., 2017, Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 258171297