Dependent type refinements for futures

DOI10.46298/ENTICS.12286MaRDI QIDQ6831460zbMATH OpenFDO

Authors Siva Somayyajula, Frank Pfenning

Publication date 2 April 2026

Copyright license arXiv.org Non-exclusive license to distribute

Full work available at URL https://doi.org/10.46298/ENTICS.12286

zbMATH Keywords

futurespartial correctnesssequent calculustype refinements

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites work

• A Hoare Logic for Call-by-Value Functional Programs
• A Sequent Calculus for Type Theory
• Abstract refinement types
• Analytic cut
• Automated Reasoning with Analytic Tableaux and Related Methods
• Certifying data in multiparty session types
• Communicating state transition systems for fine-grained concurrent resources
• CONCUR 2004 - Concurrency Theory
• Copatterns, programming infinite structures by observations
• Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocols
• Depending on session-typed processes
• Foundations of regular coinduction
• Hidden coinduction: behavioural correctness proofs for objects
• Higher-order processes, functions, and sessions: a monadic integration
• scientific article; zbMATH DE number 2185708 (Why is no real title available?)
• scientific article; zbMATH DE number 3758289 (Why is no real title available?)
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Mathematics of program construction. 10th international conference, MPC 2010, Québec City, Canada, June 21--23, 2010. Proceedings
• MULTILISP: a language for concurrent symbolic computation
• Polarized subtyping
• Practical foundations for programming languages
• Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016
• Program verification by coinduction
• Programming Languages and Systems
• Proof of correctness of data representations
• Refinement types for Haskell
• Relating state-based and process-based concurrency through linear logic (full-version)
• Semi-axiomatic sequent calculus
• Session Types with Arithmetic Refinements
• Telescopic mappings in typed lambda calculus
• Tridirectional typechecking
• Type-based termination for futures
• Types for Proofs and Programs
• Well-definedness and observational equivalence for inductive–coinductive programs

This page was built for publication: Dependent type refinements for futures

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