Type soundness proofs with definitional interpreters

DOI10.1145/3009837.3009866zbMath1380.68111OpenAlexW2560908054MaRDI QIDQ5370900

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

DOTtype soundnessScaladefinitional interpretersdependent object types

Mathematics Subject Classification ID

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

Related Items (2)

Soundness Conditions for Big-Step Semantics ⋮ The Essence of Dependent Object Types

Uses Software

• Coq

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