Some Domain Theory and Denotational Semantics in Coq

DOI10.1007/978-3-642-03359-9_10zbMath1252.68248OpenAlexW1813662263MaRDI QIDQ3183523

Nick Benton, Carsten Varming, Andrew J. Kennedy

Publication date: 20 October 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_10

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Continuous lattices and posets, applications (06B35)

Related Items

The Scott model of PCF in univalent type theory ⋮ A Purely Definitional Universal Domain ⋮ Strongly typed term representations in Coq ⋮ Apartness, sharp elements, and the Scott topology of domains ⋮ A model of PCF in guarded type theory ⋮ Partiality, Revisited ⋮ Representing model theory in a type-theoretical logical framework ⋮ A logical framework combining model and proof theory ⋮ A Certified Study of a Reversible Programming Language

Uses Software

• Coq
• LCF

Cites Work

• Notions of computation and monads
• The geometry of tensor calculus. I
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Relational properties of domains
• Formalizing synthetic domain theory. The basic definitions
• Biorthogonality, step-indexing and compiler correctness
• Proofs of Randomized Algorithms in Coq
• HOLCF = HOL + LCF
• General Recursion via Coinductive Types
• Higher-Order Separation Logic in Isabelle/HOLCF
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item