Dependent types and fibred computational effects

DOI10.1007/978-3-662-49630-5_3MaRDI QIDQ2811331zbMATH OpenOpenAlexFDO

Authors Danel Ahman, Neil Ghani, Gordon D. Plotkin

Publication date 10 June 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.com/chapter/10.1007/978-3-662-49630-5_3

Mathematics Subject Classification ID

Type theory (03B38) Logic in computer science (03B70) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Dependent types in mathematical theory of programming
• Dependent inductive and coinductive types are fibrational dialgebras
• Normalization by evaluation and algebraic effects
• Fibrational modal type theory
• scientific article; zbMATH DE number 2090721

Cites work

• A categorical semantics for linear logical frameworks
• A dependent type theory with abstractable names
• Algebras for parameterised monads
• Categorical logic and type theory
• Combining effects: sum and tensor
• Combining proofs and programs in a dependently typed language
• Continuous Lattices and Domains
• Countable Lawvere theories and computational effects
• Handling algebraic effects
• Hoare type theory, polymorphism and separation
• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 2087441 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• scientific article; zbMATH DE number 822489 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• Indexed induction and coinduction, fibrationally
• Instances of computational effects: an algebraic perspective
• Integrating linear and dependent types
• Monadic parsing in Haskell
• Notions of computation and monads
• Programming and reasoning with algebraic effects and dependent types
• Semantics for algebraic operations
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The enriched effect calculus: syntax and semantics

Cited in

(9)

• A general semantic construction of dependent refinement type systems, categorically
• A classical sequent calculus with dependent types
• ν-Types for Effects and Freshness Analysis
• Gradual type theory
• An effectful way to eliminate addiction to dependence
• Call-by-name gradual type theory
• No value restriction is needed for algebraic effects and handlers
• CHAD for expressive total languages
• Monoidal closure of Grothendieck constructions via -tractable monoidal structures and Dialectica formulas

This page was built for publication: Dependent types and fibred computational effects

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