Picture of classic books on shelf

Literary linguistics: Open Access research in English language

Strathprints makes available Open Access scholarly outputs by English Studies at Strathclyde. Particular research specialisms include literary linguistics, the study of literary texts using techniques drawn from linguistics and cognitive science.

The team also demonstrates research expertise in Renaissance studies, researching Renaissance literature, the history of ideas and language and cultural history. English hosts the Centre for Literature, Culture & Place which explores literature and its relationships with geography, space, landscape, travel, architecture, and the environment.

Explore all Strathclyde Open Access research...

Program extraction from nested definitions

Miyamoto, Kenji and Nordvall Forsberg, Fredrik and Schwichtenberg, Helmut (2013) Program extraction from nested definitions. In: Interactive Theorem Proving. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, Berlin, pp. 370-385. ISBN 9783642396335

Full text not available in this repository. Request a copy from the Strathclyde author

Abstract

Minlog is a proof assistant which automatically extracts computational content in an extension of Gödel’s T from formalized proofs. We report on extending Minlog to deal with predicates defined using a particular combination of induction and coinduction, via so-called nested definitions. In order to increase the efficiency of the extracted programs, we have also implemented a feature to translate terms into Haskell programs. To illustrate our theory and implementation, a formalisation of a theory of uniformly continuous functions due to Berger is presented.