Tridirectional typechecking

DOI10.1145/964001.964025MaRDI QIDQ3452267zbMATH OpenOpenAlexFDO

Authors 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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• Complete and easy bidirectional typechecking for higher-rank polymorphism
• A bidirectional refinement type system for LF
• scientific article; zbMATH DE number 1538022
• Let arguments go first
• A semantics for type checking

Cited in

(13)

• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Let arguments go first
• Complete and easy bidirectional typechecking for higher-rank polymorphism
• Termination checking with types
• Graded modal dependent type theory
• Preemptive Type Checking in Dynamically Typed Languages
• Polarized subtyping
• Refinement Types as Proof Irrelevance
• Set constraints, pattern match analysis, and SMT
• Extensible Datasort Refinements
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• On the Values of Reducibility Candidates
• On the unity of duality

Describes a project that uses

Uses Software

• Forsythe

This page was built for publication: Tridirectional typechecking

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