Tridirectional typechecking

DOI10.1145/964001.964025zbMath1325.68062OpenAlexW2296725671MaRDI QIDQ3452267

Joshua Dunfield, Frank Pfenning

Publication date: 11 November 2015

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

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

zbMATH Keywords

dependent typesintersection typestype refinementsunion types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

Set Constraints, Pattern Match Analysis, and SMT ⋮ Polarized subtyping ⋮ Extensible Datasort Refinements ⋮ Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage ⋮ Graded modal dependent type theory ⋮ Termination checking with types ⋮ On the unity of duality ⋮ Refinement Types as Proof Irrelevance ⋮ On the Values of Reducibility Candidates ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

• Forsythe

This page was built for publication: Tridirectional typechecking