Extensible Datasort Refinements

DOI10.1007/978-3-662-54434-1_18zbMath1485.68062arXiv1701.02842OpenAlexW2577120732MaRDI QIDQ2988653

Joshua Dunfield

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1701.02842

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Beluga
• Twelf
• Stardust
• Delphin
• Forsythe
• GitHub

Cites Work

• Intersection types and computational effects
• Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance
• Tridirectional typechecking
• A framework for defining logics
• Complete and easy bidirectional typechecking for higher-rank polymorphism
• Abstract Refinement Types
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Unnamed Item

This page was built for publication: Extensible Datasort Refinements