Dependent Types and Fibred Computational Effects

DOI10.1007/978-3-662-49630-5_3zbMath1475.68057OpenAlexW2460339236MaRDI QIDQ2811331

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

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

Related Items (6)

Unnamed Item ⋮ CHAD for expressive total languages ⋮ No value restriction is needed for algebraic effects and handlers ⋮ A Classical Sequent Calculus with Dependent Types ⋮ A general semantic construction of dependent refinement type systems, categorically ⋮ Gradual type theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A dependent type theory with abstractable names
• Notions of computation and monads
• Categorical logic and type theory
• Combining effects: sum and tensor
• Integrating Linear and Dependent Types
• Handling Algebraic Effects
• Algebras for Parameterised Monads
• The enriched effect calculus: syntax and semantics
• A Categorical Semantics for Linear Logical Frameworks
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• Hoare type theory, polymorphism and separation
• Monadic parsing in Haskell
• Continuous Lattices and Domains
• Semantics for Algebraic Operations
• Programming and reasoning with algebraic effects and dependent types
• Instances of Computational Effects: An Algebraic Perspective
• Combining proofs and programs in a dependently typed language
• Indexed Induction and Coinduction, Fibrationally

This page was built for publication: Dependent Types and Fibred Computational Effects