Towards a mechanized metatheory of standard ML

DOI10.1145/1190216.1190245zbMath1295.68088OpenAlexW3163573021MaRDI QIDQ3189797

Karl Crary, Daniel K. Lee, Robert Harper

Publication date: 12 September 2014

Published in: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

logical frameworkstype safetyStandard MLmechanized metatheoryTwelflanguage definitions

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (20)

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ The Twelf Proof Assistant ⋮ A Rewriting Logic Approach to Type Inference ⋮ Certified Static Analysis by Abstract Interpretation ⋮ Mechanized semantics for the clight subset of the C language ⋮ A scalable module system ⋮ CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Nested abstract syntax in Coq ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ SMT proof checking using a logical framework ⋮ Representing model theory in a type-theoretical logical framework ⋮ Syntactic Metatheory of Higher-Order Subtyping ⋮ Programming Inductive Proofs ⋮ Explicit Contexts in LF (Extended Abstract) ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle ⋮ Harpoon: mechanizing metatheory interactively ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf

This page was built for publication: Towards a mechanized metatheory of standard ML