Interactive programming in Agda -- objects and graphical user interfaces

DOI10.1017/S0956796816000319MaRDI QIDQ5372002zbMATH OpenOpenAlexFDO

Authors Andreas Abel, Stephan Adelsberger, Anton Setzer

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796816000319

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1670486
• scientific article; zbMATH DE number 2247254
• State dependent IO-monads in type theory
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Types for Proofs and Programs

Cites work

• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 2185666 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 1189292 (Why is no real title available?)
• scientific article; zbMATH DE number 1223720 (Why is no real title available?)
• scientific article; zbMATH DE number 1178950 (Why is no real title available?)
• scientific article; zbMATH DE number 1956503 (Why is no real title available?)
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• scientific article; zbMATH DE number 2247254 (Why is no real title available?)
• A predicative analysis of structural recursion
• A set constructor for inductive sets in Martin-Löf's type theory
• Coalgebras as types determined by their elimination rules
• Codatatypes in ML
• Copatterns, programming infinite structures by observations
• Foundational extensible corecursion: a proof assistant perspective
• How to reason coinductively informally
• Indexed containers
• Induction-recursion and initial algebras.
• Inductive families
• Inductive-inductive definitions
• Mixed Inductive/Coinductive Types and Strong Normalization
• Notions of computation and monads
• Programming interfaces and basic topology
• Programming with algebraic effects and handlers
• Rewriting Techniques and Applications
• Safe functional reactive programming through dependent types
• Semi-continuous Sized Types and Termination
• Small induction recursion
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• The view from the left
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Type-Based Termination with Sized Products
• Type-based termination of recursive definitions
• Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
• Typed Lambda Calculi and Applications
• Typestate: A programming language concept for enhancing software reliability
• Wellfounded recursion with copatterns: a unified approach to termination and productivity

Cited in

(6)

• A semantic model for graphical user interfaces
• Programming graphical user interfaces with Scheme
• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 2247254 (Why is no real title available?)
• Undecidability of equality for codata types
• State dependent IO-monads in type theory

Describes a project that uses

Uses Software

• Coq
• Haskell
• Agda
• wxHaskell
• MiniAgda
• Eff
• GitHub

This page was built for publication: Interactive programming in Agda -- objects and graphical user interfaces

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