Related papers: Proceedings Types for Proofs and Programs, Revised…
The first objective of this paper is to present and discuss various types of models of program understanding. They are discussed in relation to models of text understanding. The second objective of this paper is to assess the effect of…
Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential to enforcing program correctness; by relying on sequencing constructs, a session type can precisely…
We present {\lambda}ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs…
We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be…
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are solicited in all areas of logic programming and related areas, including but…
Humans can generate reasonable answers to novel queries (Schulz, 2012): if I asked you what kind of food you want to eat for lunch, you would respond with a food, not a time. The thought that one would respond "After 4pm" to "What would you…
Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide…
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have…
To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $\pi$-calculus by means of a suitable encoding. The encoding allows one to reuse results…
Refinement types -- types qualified with logical predicates -- have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these systems refinements are either written in a separate…
Generative pre-trained models power intelligent software features used by millions of users controlled by developer-written natural language prompts. Despite the impact of prompt-powered software, little is known about its development…
In recent years, the interest in using proof assistants to formalise and reason about mathematics and programming languages has grown. Type-logical grammars, being closely related to type theories and systems used in functional programming,…
The subject of this work is quantum predicative programming -- the study of developing of programs intended for execution on a quantum computer. We look at programming in the context of formal methods of program development, or programming…
This volume contains a final and revised selection of papers presented at the Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), held in Vienna (Austria) on July 18th, affiliated with TLCA 2014, Typed Lambda Calculi and…
This volume contains the proceedings of PLACES 2025, the 16th edition of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The workshop is scheduled to take place in Hamilton, Canada, on May…
This volume contains a selection of papers presented at Linearity&TLLA 2020, namely the Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, held on June 29-30, 2020 online. (The workshop was supposed…
This volume contains a selection of the papers presented at the XVI Jornadas sobre Programaci\'on y Lenguajes (PROLE 2016), held at Salamanca, Spain, during September 14th-15th, 2016. Previous editions of the workshop were held in Santander…
Type-level programming is an increasingly popular way to obtain additional type safety. Unfortunately, it remains a second-class citizen in the majority of industrially-used programming languages. We propose a new dependently-typed system…
It is discussed a practical possibility of a provable programming of mathematics basing on intuitionism and the dependent types feature of a programming language.The principles of constructive mathematics and provable programming are…
This volume contains selected papers presented at the 9th International Workshop on Reduction Strategies in Rewriting and Programming, WRS2009, which was held in Brasilia on the 28th June 2009, associated to RTA 2009 (the 20th International…