To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Well-founded recursion ov… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

Well-founded recursion over contextual objects

Conference paper
Authors Brigitte Pientka
Andreas Abel
Published in Leibniz International Proceedings in Informatics, LIPIcs
ISSN 1868-8969
Publication year 2015
Published at Department of Computer Science and Engineering (GU)
Language en
Keywords Dependent types, Logical frameworks, Type systems
Subject categories Computer and Information Science

Abstract

© Brigitte Pientka and Andreas Abel;.We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?