56 research outputs found
JLimperg/msc-thesis-code: v1.0
No full textCompanion formalisation of the Master thesis A Reflexive Graph Model of Sized Types.</p
JLimperg/well-founded-corecursion: v0.0.2
No full textAn attempt to integrate well-founded recursion into corecursio
A Reflexive Graph Model of Sized Types
Full text linkSized types are a type-based termination checking mechanism for dependently typed languages.
Compared to syntactic termination checkers, sized types make termination checking
more modular and allow for an elegant treatment of coinductive and nested data types.
This thesis investigates λST, a simply-typed lambda calculus with sized types similar to
those of Agda. Its primary contribution is a relationally parametric denotational semantics
for λST in the form of a reflexive graph model. In this model, sizes are irrelevant: they do
not affect the result of any computations. The calculus and model are fully formalised in
Agda (without sized types)
A novice-friendly induction tactic for lean
No full textIn theorem provers based on dependent type theory such as Coq and Lean, induction is a fundamental proof method and induction tactics are omnipresent in proof scripts. Yet the ergonomics of existing induction tactics are not ideal: they do not reliably support inductive predicates and relations; they sometimes generate overly specific or unnecessarily complex induction hypotheses; and they occasionally choose confusing names for the hypotheses they introduce. This paper describes a new induction tactic, implemented in Lean 3, which addresses these issues. The tactic is particularly suitable for educational use, but experts should also find it more convenient than existing induction tactics. In addition, the tactic serves as a moderately complex case study for the metaprogramming framework of Lean 3. The paper describes some difficulties encountered during the implementation and suggests improvements to the framework
Aesop: White-Box Best-First Proof Search for Lean
No full textThis is a preprint of the paper "Aesop: White-Box Best-First Proof Search for Lean", to be presented at CPP 2023. The published version will be available at doi:10.1145/3573105.3575671.Partly funded by NWO grant 016.Vidi.189.037 (Lean Forward)
"Libertà o Morte W Marat W Robespierre" : note di contesto per un'opera di Jannis Kounellis
Full text linkThe article considers Jannis Kounellis’ Untitled (Freedom or Death. Long live Marat Long live Robespierre), created in 1969 and exhibited in Naples in that year. The author focuses on its possible visual antecedents, comparing it with contemporary works by Italian and international artists and analyzing the content of the prominent inscription, with a reconstruction of its historical, political and literary allusions, thus clarifying the meaning it had in Italy at the end of the 1960s. Untitled is also briefly discussed in the context of French revolutionary art
Aesop: White-Box Best-First Proof Search for Lean
No full textWe present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be. Since we use a best-first search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for best-first search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows
Code choice and code-switching in Swiss-German internet relay chat rooms
No full textIn the German-speaking regions of Switzerland, dialect is spoken by all social groups in most communicative situations, Standard German being used only when prescribed. Swiss dialects rarely appeared in written form before the 1980s, apart from the genre of dialect literature. Due to the growing acceptance of informal writing styles in many European languages, dialect is increasingly employed for written personal communication, in particular in computer-mediated communication (CMC). In Swiss Internet Relay Chat (IRC) rooms, varieties of German are used side by side as all chatters have a command of both standard and dialectal varieties. Depending on the channel, the proportion of dialectal contributions can be as high as 90 percent. The choice of a particular variety depends on both individual preference and on the predominant variety used within a specific thread. In this paper I take a quantitative approach to language variation in IRC and demonstrate how such an approach can help embed qualitative research on code-switching in CMC
The Consequences of Information: Institutional Implications of Technological Change
No full textExtended review of the book by professor Jannis Kallinikos, London School of Economics and Political Science. The critical review highlights the strenghts and weaknesses of the argument developed by the author
- …
