Tridirectional typechecking

DOI10.1145/964001.964025zbMATH Open1325.68062OpenAlexW2296725671MaRDI QIDQ3452267FDOQ3452267

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

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

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)

Cited In (13)

• 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
• 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

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