Combining proofs and programs in a dependently typed language

DOI10.1145/2535838.2535883zbMath1284.68125OpenAlexW2048536148MaRDI QIDQ5408400

Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cis_reports/985

zbMATH Keywords

terminationdependent typesgeneral recursion

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (7)

LF+ in Coq for "fast and loose" reasoning ⋮ Implementing Cantor’s Paradise ⋮ Unified Syntax with Iso-types ⋮ Unnamed Item ⋮ Fibrational modal type theory ⋮ A Classical Realizability Model for a Semantical Value Restriction ⋮ Dependent Types and Fibred Computational Effects

Uses Software

• Coq
• Haskell
• Epigram
• Agda
• Irdis
• AURA
• Ynot

This page was built for publication: Combining proofs and programs in a dependently typed language