Type soundness proofs with definitional interpreters

DOI10.1145/3009837.3009866MaRDI QIDQ5370900zbMATH OpenOpenAlexFDO

Authors Nada Amin, Tiark Rompf

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3009837.3009866

zbMATH Keywords

definitional interpretersdependent object typesDOTScalatype soundness

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A very modal model of a modern, major, general type system
• The essence of dependent object types
• Type soundness for path polymorphism
• A simplified account of polymorphic references
• Syntactic soundness proof of a type-and-capability system with hidden state

Cited in

(4)

• The essence of dependent object types
• scientific article; zbMATH DE number 1980941 (Why is no real title available?)
• Soundness conditions for big-step semantics
• Recursive subtyping for all

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Type soundness proofs with definitional interpreters

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370900)