Search events for 'all'
Bimodels and Biorthogonality for Abstract Machines
ICFP Papers People: April Tune, Alex Kavvos
… the CK and CEK machines, all as corollaries. All results are mechanized in Agda. …
Exploring First-Class Constrained Types: Semantics, Type Inference, and a Characterization of Termination
ICFP Papers People: Chun Kit Lam, Florent Ferrari-Dominguez, Lionel Parreaux
… exhibits interesting properties. First, all well-typed FCCT terms terminate under …. Second, all CBN-terminating terms are well-typed in FCCT. Together, these two … approximation by sharing polymorphic instantiations, ensuring termination on all input …
A Catenable, Splittable, Transient Sequence Data Structure
ICFP Papers People: Arthur Charguéraud, François Pottier
… for a one-size-fits-all, general-purpose sequence data structure. …
Coverage Types Modulo Equivalences
ICFP SRC People: Aaryan Prakash, Benjamin Delaware
… they enforce all distinct inputs must be generated. We propose an extension …
Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations
ICFP Papers People: Patrick Bahr
… for all source programs is too strong a requirement for complex source languages … calculation techniques, all while maintaining the same strong correctness guarantees …
QuickChecking Convergence of Rewriting Systems (Functional Pearl)
ICFP Papers People: Koen Claessen
… here: exhaustively computing all normal forms is fundamentally flawed and too slow …
Completeness of Iris-Based Program Logics
ICFP Papers People: Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, Joseph Tassarotti
… ), and a relational logic for proving refinement. All our results have been mechanized …
A Separation Logic for Parallel Time Complexity with Work and Span Credits
ICFP Papers People: Alexandre Moine, Sam Westrick, Joseph Tassarotti
… concurrency with parallelism. All the presented results are mechanized in the Rocq …