pith. sign in

arxiv: 2512.04755 · v2 · submitted 2025-12-04 · 💻 cs.PL

Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts

Stian Lybech , Daniele Gorla , Luca Aceto This is my paper

Pith reviewed 2026-05-17 01:58 UTC · model grok-4.3

classification 💻 cs.PL
keywords smart contractstype safetysemantic typingproof-carrying codefallback functionsinformation flow controlnon-interferenceTinySol
0
0 comments X

The pith

Smart contract creators can attach formal proof certificates to ensure type safety for fallback functions on the blockchain.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops semantic typing for smart contracts so that code using statically untypable constructs such as fallback functions can still be shown to satisfy type safety. The creator supplies a formal proof of safety expressed in terms of the semantics of types, and users of the contract only need to check the validity of that proof certificate. This proof-carrying approach is demonstrated on TinySol, a distilled Solidity, where it enforces information flow control and non-interference through security types whose proofs are given as compact coinductive typing interpretations.

Core claim

The semantics of types are given by a typed operational semantics of TinySol, and proofs of safety are expressed as coinductively-defined typing interpretations that can be represented compactly via up-to techniques; the same machinery types the pointer-to-implementation pattern based on fallback functions and rejects a distilled version of the Parity Multisig Wallet Attack.

What carries the argument

Coinductively-defined typing interpretations, represented compactly via up-to techniques, that interpret the typed operational semantics of TinySol.

If this is right

  • Contract creators can equip code containing fallback functions with a compact proof certificate of type safety.
  • Users verify only the certificate rather than re-checking the full code.
  • The pointer-to-implementation pattern can be given a type-safe account based on the fallback function.
  • A distilled form of the Parity Multisig Wallet Attack is rejected by the typing machinery.
  • Information flow control and non-interference hold for TinySol programs that pass the semantic type checks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same proof-carrying technique could be lifted to full Solidity or other blockchain languages by adapting the operational semantics and up-to representation.
  • On-chain validation of compact certificates might allow lighter-weight static analysis tools for smart-contract platforms.
  • Up-to techniques for typing interpretations may transfer to other verification tasks that must be checked repeatedly on immutable ledgers.

Load-bearing premise

That users of the contract can reliably check the validity of the provided proof certificate of type safety in the immutable blockchain environment.

What would settle it

A concrete case in which a contract equipped with a valid proof certificate still permits an information-flow violation or a type error during execution of a fallback function.

Figures

Figures reproduced from arXiv: 2512.04755 by Daniele Gorla, Luca Aceto, Stian Lybech.

Figure 1
Figure 1. Figure 1: The syntax of TinySol. 2 The TinySol language and its security types 2.1 Typed Syntax We use an extended version of the TinySol language, based on the presentation in [1], which, in turn, is based on the original presentation in [6]. Its syntax is given in [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Typed operational semantics of stacks (1). [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Typed operational semantics of stacks (2): method calls [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The semantic type rule for fallback function calls. [PITH_FULL_IMAGE:figures/full_fig_p017_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: An example of the pointer-to-implementation pattern. [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: An example with safe encapsulation of variadic arguments. [PITH_FULL_IMAGE:figures/full_fig_p019_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: A proxy contract using both explicit forwarding and fallback. [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: An example where id is used as the method name. func update ( x ) { this . impl := x } thus permitting an unrestricted information flow into impl, the appropriate security setting in the implementation interface 𝐼 𝑋 would be to declare impl : var(𝐼 𝑋,𝑈 ) update : proc( (𝐼 𝑋,𝑈 )):𝑈 In that case, forwarding Proxy.update to X.update with a delegate call would lead to an informa￾tion flow from an Untrusted var… view at source ↗
Figure 9
Figure 9. Figure 9: Semantics of declarations. The semantics of expression configurations has the form ⟨𝑒, env𝑆𝑉 ⟩ → 𝑣 and is standard; its defining rules are in [PITH_FULL_IMAGE:figures/full_fig_p027_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Semantics of expressions; for the sake of simplicity, we here assume that [PITH_FULL_IMAGE:figures/full_fig_p027_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Small-step semantics of stacks (to be completed with the rules depicted in Figure [PITH_FULL_IMAGE:figures/full_fig_p028_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Small-step semantics of stacks: method calls [PITH_FULL_IMAGE:figures/full_fig_p029_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Consistency rules for Σ. The judgment is of the form Σ; Γ ⊢ Σ, which expresses that the inheritance tree recorded in Σ is consistent with the actual declarations recorded in Γ. The rules are quite simple, since they just iterate through the inheritance environment, examining each entry in turn. Σ only records the inheritance hierarchy, whereas the actual structures of the interfaces are recorded in Γ. Hen… view at source ↗
Figure 14
Figure 14. Figure 14: The subtyping relation for expression types [PITH_FULL_IMAGE:figures/full_fig_p031_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Type rules for expressions. The type rules for expressions 𝑒 are given in [PITH_FULL_IMAGE:figures/full_fig_p032_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Type rules for statements env𝑉 along with the values. The extraction function E(·) simply extracts this information from the variable environment found on the stack, to build the type environment Δ ′ relative to which the , Vol. 1, No. 1, Article . Publication date: December 2025 [PITH_FULL_IMAGE:figures/full_fig_p033_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Type rules for the method-, state-, and variable environments [PITH_FULL_IMAGE:figures/full_fig_p034_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: Type rules for stacks. remainder of the stack 𝑄 is then typed. It is defined as follows: E(𝜖) = 𝜖 E(env′ 𝑉 , 𝑥 : (𝑣,𝑇 )) = E(env′ 𝑉 ) , 𝑥 : 𝑇 , Vol. 1, No. 1, Article . Publication date: December 2025 [PITH_FULL_IMAGE:figures/full_fig_p034_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Rules for the 𝑠-parameterised equivalence relation. , Vol. 1, No. 1, Article . Publication date: December 2025 [PITH_FULL_IMAGE:figures/full_fig_p035_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: The free variable names for expressions and statements. [PITH_FULL_IMAGE:figures/full_fig_p037_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: Consistency rules for env𝐹 and env𝑀 . , Vol. 1, No. 1, Article . Publication date: December 2025 [PITH_FULL_IMAGE:figures/full_fig_p037_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Consistency rules for the environments env [PITH_FULL_IMAGE:figures/full_fig_p038_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: Typed operational semantics for expressions. [PITH_FULL_IMAGE:figures/full_fig_p040_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: Well-formedness of stacks 𝑄. In [wf-stm] we require that any statement 𝑆 found on the stack must only contain names found in the domains of env𝑆𝑉 . Together with consistency of env𝑆𝑉 , this ensures that transitions cannot be stuck due to a free name, or a missing contract implementation. In [wf-del], we remove 𝑥 from env𝑉 when we encounter an end-of-scope symbol del(𝑥), since the domain of env𝑉 is used in… view at source ↗
Figure 25
Figure 25. Figure 25: Semantic type rules for code environments env [PITH_FULL_IMAGE:figures/full_fig_p072_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: Semantic subtyping rules for stacks and statements. [PITH_FULL_IMAGE:figures/full_fig_p077_26.png] view at source ↗
Figure 27
Figure 27. Figure 27: Semantic type rules for stacks. , Vol. 1, No. 1, Article . Publication date: December 2025 [PITH_FULL_IMAGE:figures/full_fig_p077_27.png] view at source ↗
Figure 28
Figure 28. Figure 28: Semantic type rules for statements (plus rule [PITH_FULL_IMAGE:figures/full_fig_p078_28.png] view at source ↗
read the original abstract

This paper develops semantic typing in a smart-contract setting to ensure type safety of code that uses statically untypable language constructs, such as the fallback function. The idea is that the creator of a contract on the blockchain equips code containing such constructs with a formal proof of its type safety, given in terms of the semantics of types. Then, a user of the contract only needs to check the validity of the provided 'proof certificate' of type safety. This is a form of proof-carrying code, which naturally fits with the immutable nature of the blockchain environment. As a concrete application of our approach, we focus on ensuring information flow control and non-interference for TinySol, a distilled version of the Solidity language, through security types. We provide the semantics of types in terms of a typed operational semantics of TinySol and we express the proofs of safety as coinductively-defined typing interpretations, which can be represented compactly via up-to techniques, similar to those used for bisimilarity. We also show how our machinery can be used to type the typical pointer-to-implementation pattern based on the fallback function and to reject a distilled version of the infamous Parity Multisig Wallet Attack.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. This paper develops a semantic typing approach for smart contracts to ensure type safety for statically untypable constructs such as fallback functions. It equips TinySol (a distilled Solidity) with a typed operational semantics for security types, expresses type-safety proofs as coinductively defined typing interpretations, and uses up-to techniques to obtain compact representations. The framework is applied to information-flow control and non-interference, to typing the pointer-to-implementation pattern, and to rejecting a distilled version of the Parity Multisig Wallet attack, all framed as proof-carrying code that exploits blockchain immutability.

Significance. If the formal development is sound, the work supplies a principled way to attach verifiable type-safety certificates to contracts containing fallback functions, thereby addressing a recurring source of vulnerabilities in Solidity-like languages. The explicit use of coinductive definitions together with up-to techniques for compactness is a technical strength that aligns with established methods in process calculi and bisimulation theory. The approach also demonstrates how semantic typing can reject known attacks while permitting useful but statically ill-typed patterns.

major comments (2)
  1. [Abstract and proof-carrying code discussion] Abstract and the section introducing proof-carrying code: the central claim that 'a user of the contract only needs to check the validity of the provided proof certificate' and that this 'naturally fits with the immutable nature of the blockchain environment' rests on the unexamined assumption that coinductive certificates can be verified feasibly inside resource-constrained, gas-limited runtimes. No bounds on certificate size, no complexity analysis of the up-to-technique reductions, and no discussion of how verification would be implemented by a Solidity-like interpreter or by other contracts are supplied; this assumption is load-bearing for the claimed practicality.
  2. [Coinductive typing interpretations] Section presenting the coinductive typing interpretations: while the paper states that proofs of safety are expressed coinductively and represented compactly via up-to techniques, it supplies no concrete derivation, no example reduction sequence, and no statement of the up-to relation or the associated proof obligations. Without these details the soundness of the non-interference and attack-rejection claims cannot be assessed directly from the manuscript.
minor comments (2)
  1. [Operational semantics] The distinction between the typed operational semantics and the underlying untyped semantics of TinySol should be made explicit with a small illustrative example early in the development.
  2. [Notation] Notation for the typing interpretations and the up-to relation would benefit from a compact summary table or diagram.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive comments. We address each major comment below and indicate planned revisions to the manuscript.

read point-by-point responses

  1. Referee: [Abstract and proof-carrying code discussion] Abstract and the section introducing proof-carrying code: the central claim that 'a user of the contract only needs to check the validity of the provided proof certificate' and that this 'naturally fits with the immutable nature of the blockchain environment' rests on the unexamined assumption that coinductive certificates can be verified feasibly inside resource-constrained, gas-limited runtimes. No bounds on certificate size, no complexity analysis of the up-to-technique reductions, and no discussion of how verification would be implemented by a Solidity-like interpreter or by other contracts are supplied; this assumption is load-bearing for the claimed practicality.

    Authors: We agree that the manuscript does not examine the practical verification costs of coinductive certificates under gas limits. The work centers on the semantic foundations of typing interpretations and their use for non-interference and attack rejection. In revision we will expand the proof-carrying code section with a high-level discussion of certificate size bounds obtainable from the up-to techniques, together with an outline of how verification could be realized by a contract interpreter. A full complexity analysis will be noted as future work. revision: partial

  2. Referee: [Coinductive typing interpretations] Section presenting the coinductive typing interpretations: while the paper states that proofs of safety are expressed coinductively and represented compactly via up-to techniques, it supplies no concrete derivation, no example reduction sequence, and no statement of the up-to relation or the associated proof obligations. Without these details the soundness of the non-interference and attack-rejection claims cannot be assessed directly from the manuscript.

    Authors: The formal definitions of the coinductive interpretations and the up-to techniques appear in the technical sections. To improve accessibility we will add a new subsection containing a concrete example: a full derivation for a minimal TinySol contract that uses a fallback function, the explicit up-to relation, the proof obligations, and a short reduction sequence illustrating compactness. revision: yes

Circularity Check

0 steps flagged

No significant circularity; semantic derivation is self-contained

full rationale

The paper constructs a typed operational semantics for TinySol and defines type safety proofs directly as coinductive typing interpretations, compactly represented via up-to techniques. These definitions and proofs are presented as independent formal machinery for proof-carrying code without any reduction to fitted parameters, self-citations that bear the central load, or prior results by the same authors. The approach stands as a direct semantic construction that does not equate its outputs to its inputs by construction, making the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard coinductive reasoning and the assumption that a typed operational semantics faithfully models TinySol execution; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • standard math Coinductive definitions suffice to represent compact proofs of type safety via up-to techniques
    Invoked when expressing proofs of safety as coinductively-defined typing interpretations
  • domain assumption The typed operational semantics of TinySol accurately captures the runtime behavior relevant to information flow
    Required for the semantics of security types to imply non-interference

pith-pipeline@v0.9.0 · 5510 in / 1282 out tokens · 38667 ms · 2026-05-17T01:58:33.293546+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

66 extracted references · 66 canonical work pages

  1. [1]

    An Algorithmic Meta Theorem for Homomorphism Indistin- guishability

    Luca Aceto, Daniele Gorla, and Stian Lybech. A sound type system for secure currency flow, 2024. URL https: //arxiv.org/abs/2405.12976v2. An extended abstract appeared in theProc. of ECOOP 2024(https://doi.org/10.4230/LIPIcs. ECOOP.2024.1)

    work page doi:10.4230/lipics 2024

  2. [2]

    Preventing out-of-gas exceptions by typing

    Luca Aceto, Daniele Gorla, Stian Lybech, and Mohammad Hamdaqa. Preventing out-of-gas exceptions by typing. InLeveraging Applications of Formal Methods, Verification and Validation, pages 409–426. Springer, 2025. URL https: //doi.org/10.1007/978-3-031-73709-1_25

    work page doi:10.1007/978-3-031-73709-1_25 2025

  3. [3]

    PhD thesis, Princeton University, 2004

    Amal Jamil Ahmed.Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. URL http://www.ccs. neu.edu/home/amal/ahmedsthesis.pdf

    work page 2004

  4. [4]

    Appel and David McAllester

    Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657–683, September 2001. URL https://doi.org/10.1145/504709.504712

    work page doi:10.1145/504709.504712 2001

  5. [5]

    PhD thesis, Royal Institute of Technology, Stockholm, Sweden, 2014

    Musard Balliu.Logics for Information Flow Security:From Specification to Verification. PhD thesis, Royal Institute of Technology, Stockholm, Sweden, 2014. URL https://nbn-resolving.org/urn:nbn:se:kth:diva-150423

    work page 2014

  6. [6]

    A minimal core calculus for solidity contracts

    Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia. A minimal core calculus for solidity contracts. In Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 233–243. Springer, 2019. URL https: //doi.org/10.1007/978-3-030-31500-9_15

    work page doi:10.1007/978-3-030-31500-9_15 2019

  7. [7]

    Secure information flow and program logics

    Lennart Beringer and Martin Hofmann. Secure information flow and program logics. In20th IEEE Computer Security Foundations Symposium, CSF 2007, pages 233–248. IEEE Computer Society, 2007. URL https://doi.org/10.1109/CSF.2007. 30

    work page doi:10.1109/csf.2007 2007

  8. [8]

    Up-to techniques for weighted systems

    Filippo Bonchi, Barbara König, and Sebastian Küpper. Up-to techniques for weighted systems. InProc. of TACAS, volume 10205 ofLNCS, pages 535–552, 2017. URL https://doi.org/10.1007/978-3-662-54577-5_31

    work page doi:10.1007/978-3-662-54577-5_31 2017

  9. [9]

    A pseudo-quasi-polynomial algorithm for mean-payoff parity games , booktitle =

    Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, and Dusko Pavlovic. Sound up-to techniques and complete abstract domains. InProc. of LICS, pages 175–184. ACM, 2018. URL https://doi.org/10.1145/3209108.3209169

    work page doi:10.1145/3209108.3209169 2018

  10. [10]

    Behavioral and spatial observations in a logic for the 𝜋-calculus

    Luis Caires. Behavioral and spatial observations in a logic for the 𝜋-calculus. InFoundations of Software Science and Computation Structures, pages 72–89. Springer, 2004. URL https://doi.org/10.1007/978-3-540-24727-2_7

    work page doi:10.1007/978-3-540-24727-2_7 2004

  11. [11]

    Logical semantics of types for concurrency

    Luis Caires. Logical semantics of types for concurrency. InAlgebra and Coalgebra in Computer Science, pages 16–35. Springer, 08 2007. URL https://doi.org/10.1007/978-3-540-73859-6_2

    work page doi:10.1007/978-3-540-73859-6_2 2007

  12. [12]

    A spatial logic for concurrency (part I).Information and Computation, 186(2):194–235,

    Luis Caires and Luca Cardelli. A spatial logic for concurrency (part I).Information and Computation, 186(2):194–235,

    work page

  13. [13]

    URL https://doi.org/10.1016/S0890-5401(03)00137-8

    work page doi:10.1016/s0890-5401(03)00137-8

  14. [14]

    A spatial logic for concurrency (part II).Theoretical Computer Science, 322(3):517–565,

    Luis Caires and Luca Cardelli. A spatial logic for concurrency (part II).Theoretical Computer Science, 322(3):517–565,

    work page

  15. [15]

    URL https://doi.org/10.1016/j.tcs.2003.10.041. , Vol. 1, No. 1, Article . Publication date: December 2025. Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts 25

    work page doi:10.1016/j.tcs.2003.10.041 2003

  16. [16]

    Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. Gradual typing: a new perspective.Proc. ACM Program. Lang., 3(POPL):16:1–16:32, 2019. URL https://doi.org/10.1145/3290329

    work page doi:10.1145/3290329 2019

  17. [17]

    Up-to techniques for generalized bisimu- lation metrics

    Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-to techniques for generalized bisimu- lation metrics. InProd. of CONCUR, volume 59 ofLIPIcs, pages 35:1–35:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL https://doi.org/10.4230/LIPIcs.CONCUR.2016.35

    work page doi:10.4230/lipics.concur.2016.35 2016

  18. [18]

    R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith.Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., USA, 1986. ISBN 0134518322

    work page 1986

  19. [19]

    Up-to techniques using sized types.Proc

    Nils Anders Danielsson. Up-to techniques using sized types.Proc. ACM Program. Lang., 2(POPL):43:1–43:28, 2018. URL https://doi.org/10.1145/3158131

    work page doi:10.1145/3158131 2018

  20. [20]

    Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments,

    Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, 2021. URL https://doi.org/10.1109/ LICS52264.2021.9470654

    work page arXiv 2021

  21. [21]

    Solidity documentation

    Ethereum Foundation. Solidity documentation. https://docs.soliditylang.org/, 2022. Accessed: 2025-07-01

    work page 2022

  22. [22]

    Carlini, N., Liu, C., Erlingsson, ´U., Kos, J., and Song, D

    Dan Frumin, Robbert Krebbers, and Lars Birkedal. Compositional non-interference for fine-grained concurrent programs. In42nd IEEE Symposium on Security and Privacy, SP 2021, pages 1416–1433. IEEE, 2021. URL https: //doi.org/10.1109/SP40001.2021.00003

    work page doi:10.1109/sp40001.2021.00003 2021

  23. [23]

    J. A. Goguen and J. Meseguer. Security policies and security models. In1982 IEEE Symposium on Security and Privacy, pages 11–20, 1982. URL https://doi.org/10.1109/SP.1982.10014

    work page doi:10.1109/sp.1982.10014 1982

  24. [24]

    Mechanized logical relations for termination- insensitive noninterference.Proc

    Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. Mechanized logical relations for termination- insensitive noninterference.Proc. ACM Program. Lang., 5(POPL):1–29, 2021. URL https://doi.org/10.1145/3434291

    work page doi:10.1145/3434291 2021

  25. [25]

    A semantic framework for the security analysis of Ethereum smart contracts

    Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. A semantic framework for the security analysis of Ethereum smart contracts. In Lujo Bauer and Ralf Küsters, editors,Principles of Security and Trust, pages 243–269, Cham, 2018. Springer International Publishing. ISBN 978-3-319-89722-6

    work page 2018

  26. [26]

    A security type verifier for smart contracts.Computers & Security, 108:102343, 2021

    Xinwen Hu, Yi Zhuang, Shang-Wei Lin, Fuyuan Zhang, Shuanglong Kan, and Zining Cao. A security type verifier for smart contracts.Computers & Security, 108:102343, 2021. URL https://doi.org/10.1016/j.cose.2021.102343

    work page doi:10.1016/j.cose.2021.102343 2021

  27. [27]

    Rustbelt: securing the foundations of the rust programming language.Proc

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: securing the foundations of the rust programming language.Proc. ACM Program. Lang., 2(POPL), 2017. URL https://doi.org/10.1145/3158154

    work page doi:10.1145/3158154 2017

  28. [28]

    Iris from the ground up: A modular foundation for higher-order concurrent separation logic.Journal of Functional Programming, 28:e20,

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic.Journal of Functional Programming, 28:e20,

    work page

  29. [29]

    URL https://doi.org/10.1017/S0956796818000151

    work page doi:10.1017/s0956796818000151

  30. [30]

    Restricted permutations

    Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The essence of higher- order concurrent separation logic. InProc. of ESOP, pages 696–723. Springer, 2017. URL https://doi.org/10.1007/978-3- 662-54434-1_26

    work page doi:10.1007/978-3- 2017

  31. [31]

    Solidity security: A comprehensive list of known attack vectors and common anti-patterns, 2018

    Adrian Manning. Solidity security: A comprehensive list of known attack vectors and common anti-patterns, 2018. URL https://blog.sigmaprime.io/solidity-security.html

    work page 2018

  32. [32]

    Constructive mathematics and computer programming

    Per Martin-Löf. Constructive mathematics and computer programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors,Logic, Methodology and Philosophy of Science VI, volume 104 ofStudies in Logic and the Foundations of Mathematics, pages 153–175. Elsevier, 1982. URL https://doi.org/10.1016/S0049-237X(09)70189-2

    work page doi:10.1016/s0049-237x(09)70189-2 1982

  33. [33]

    PHI Series in Computer Science

    Robin Milner.Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, 1989. ISBN 978-0-13- 115007-2

    work page 1989

  34. [34]

    The polyadic 𝜋-calculus: a tutorial

    Robin Milner. The polyadic 𝜋-calculus: a tutorial. InLogic and Algebra of Specification, pages 203–246. Springer Berlin Heidelberg, 1993. URL https://doi.org/10.1007/978-3-642-58041-3_6

    work page doi:10.1007/978-3-642-58041-3_6 1993

  35. [35]

    A calculus of mobile processes, i.Information and Computation, 100 (1):1–40, 1992

    Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, i.Information and Computation, 100 (1):1–40, 1992. URL https://doi.org/10.1016/0890-5401(92)90008-4

    work page doi:10.1016/0890-5401(92)90008-4 1992

  36. [36]

    George C. Necula. Proof-carrying code. InProc. of POPL, page 106–119. ACM, 1997. URL https://doi.org/10.1145/ 263699.263712

    work page arXiv 1997

  37. [37]

    Springer-Verlag London, 2007

    Hanne Riis Nielson and Flemming Nielson.Semantics with Applications: An Appetizer. Springer-Verlag London, 2007. URL https://doi.org/10.1007/978-1-84628-692-6

    work page doi:10.1007/978-1-84628-692-6 2007

  38. [38]

    An introduction to the 𝜋-calculus

    Joachim Parrow. An introduction to the 𝜋-calculus. InHandbook of Process Algebra, pages 479–543. Elsevier, 2001. URL https://doi.org/10.1016/B978-044482830-9/50026-6

    work page doi:10.1016/b978-044482830-9/50026-6 2001

  39. [39]

    Lambda-definability and logical relations, 1973

    Gordon Plotkin. Lambda-definability and logical relations, 1973. URL https://www.cl.cam.ac.uk/~nk480/plotkin-logical- relations.pdf

    work page 1973

  40. [40]

    Enhancements of the bisimulation proof method

    Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors,Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science, pages 233–289. Cambridge University Press, 2011. URL https://doi.org/10.1017/cbo9780511792588.007. , Vol. 1, No. 1, Article . Publica...

    work page doi:10.1017/cbo9780511792588.007 2011

  41. [41]

    PhD thesis, Reykjavík University, December 2024

    Ilham Ahmed Qasse.Immutable Yet Mutable: Empirical Studies in Smart Contract Upgradeability. PhD thesis, Reykjavík University, December 2024. URL https://iris.landsbokasafn.is/en/publications/immutable-yet-mutable-empirical- studies-in-smart-contract-upgrade

    work page 2024

  42. [42]

    On the expressiveness and semantics of information flow types.J

    Vineet Rajani and Deepak Garg. On the expressiveness and semantics of information flow types.J. Comput. Secur., 28 (1):129–156, 2020. URL https://doi.org/10.3233/JCS-191382. An extended abstract appeared inIEEE CSF 2018

    work page doi:10.3233/jcs-191382 2020

  43. [43]

    Cambridge University Press, 2011

    Davide Sangiorgi.Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. URL https: //doi.org/10.1017/CBO9780511777110

    work page doi:10.1017/cbo9780511777110 2011

  44. [44]

    weak bisimulation up to

    Davide Sangiorgi and Robin Milner. The problem of “weak bisimulation up to”’. In Rance Cleaveland, editor,CONCUR ’92, Third International Conference on Concurrency Theory, volume 630 ofLecture Notes in Computer Science, pages 32–46. Springer, 1992. URL https://doi.org/10.1007/BFb0084781

    work page doi:10.1007/bfb0084781 1992

  45. [45]

    Environmental bisimulations for probabilistic higher-order languages.ACM Trans

    Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages.ACM Trans. Program. Lang. Syst., 41(4):22:1–22:64, 2019. URL https://doi.org/10.1145/3350618

    work page doi:10.1145/3350618 2019

  46. [46]

    Cambridge University Press, 2003

    Davide Sangiorgi and David Walker.The 𝜋 -calculus: a Theory of Mobile Processes. Cambridge University Press, 2003. URL https://doi.org/10.1017/9781316134924

    work page doi:10.1017/9781316134924 2003

  47. [47]

    Siek and Walid Taha

    Jeremy G. Siek and Walid Taha. Gradual typing for objects. InProc. ofECOOP, volume 4609 ofLNCS, pages 2–27. Springer, 2007. URL https://doi.org/10.1007/978-3-540-73589-2_2

    work page doi:10.1007/978-3-540-73589-2_2 2007

  48. [48]

    Security properties through the lens of modal logic

    Matvey Soloviev, Musard Balliu, and Roberto Guanciale. Security properties through the lens of modal logic. In37th IEEE Computer Security Foundations Symposium, CSF 2024, pages 340–355. IEEE, 2024. URL https://doi.org/10.1109/ CSF61375.2024.00009

    work page arXiv 2024

  49. [49]

    William W. Tait. Intensional interpretations of functionals of finite type I.J. Symb. Log., 32(2):198–212, 1967. URL https://doi.org/10.2307/2271658

    work page doi:10.2307/2271658 1967

  50. [50]

    A logical approach to type soundness.Journal of the ACM, 71(6), 2024

    Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A logical approach to type soundness.Journal of the ACM, 71(6), 2024. URL https://doi.org/10.1145/3676954

    work page doi:10.1145/3676954 2024

  51. [51]

    A sound type system for secure flow analysis.Journal of Computer Security, 4, 08 2000

    Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. A sound type system for secure flow analysis.Journal of Computer Security, 4, 08 2000. URL https://doi.org/10.3233/JCS-1996-42-304

    work page doi:10.3233/jcs-1996-42-304 2000

  52. [52]

    Wright and Matthias Felleisen

    Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness.Information and Computation, 115 (1):38–94, 1994. URL https://doi.org/10.1006/inco.1994.1093. , Vol. 1, No. 1, Article . Publication date: December 2025. Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts 27 A Untyped Operational Semantics The rules fo...

    work page doi:10.1006/inco.1994.1093 1994

  53. [53]

    ∪ F 𝑉 (𝑒 ′ 𝑛) ∪ F𝑉 (𝑒2) ∪ F𝑉 (𝑚) F𝑉 (dcall𝑒.𝑚(𝑒 ′ 1,

    ∪. . .∪ F 𝑉 (𝑒 ′ 𝑛) ∪ F𝑉 (𝑒2) ∪ F𝑉 (𝑚) F𝑉 (dcall𝑒.𝑚(𝑒 ′ 1, . . . , 𝑒′ 𝑛))=F 𝑉 (𝑒) ∪ F𝑉 (𝑒 ′

    work page

  54. [54]

    ∪ F 𝑉 (𝑒 ′ 𝑛) ∪ { id } F𝑉 (𝑚)= ( { id } if𝑚=id ∅otherwise Fig

    ∪. . .∪ F 𝑉 (𝑒 ′ 𝑛) ∪ { id } F𝑉 (𝑚)= ( { id } if𝑚=id ∅otherwise Fig. 20. The free variable names for expressions and statements. [c-envf1] env𝑆 ⊢env ∅ 𝐹 ⇌∅ [c-envf2] env𝑆 ⊢env ′ 𝐹 ⇌Γ ′ 𝐹 env𝑆 ⊢env ′ 𝐹 , 𝑝:𝑣⇌Γ ′ 𝐹 , 𝑝:var(𝐵 𝑠 ) where: 𝑣∈ N 𝐴 =⇒𝑣∈dom (env𝑆 ) [c-envm1] env∅ 𝑀 ⇌∅ [c-envm2] env𝑆 ⊢env ′ 𝑀 ⇌Γ ′ 𝐹 env𝑆 ⊢env ′ 𝑀, 𝑓:(e𝑥, 𝑆)⇌Γ ′ 𝑀, 𝑓:proc( e𝐵e𝑠):𝑠 w...

    work page 2025

  55. [55]

    reverse reading

    as a simple corollary of Corollaries F.4 and F.9: , Vol. 1, No. 1, Article . Publication date: December 2025. Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts 49 Corollary F.10 (Static non-interference for expressions).If •Σ;Γ;Δ⊢𝑒:𝐵 𝑠 , and •Σ;Γ;Δ⊢env 1 𝑆𝑉 ,Γ⊢env 1 𝑆𝑉 ,F 𝐴 (𝑒) ⊆dom env1 𝑆 ,F 𝑉 (𝑒) ⊆dom env1 𝑉 , and •Σ;Γ;Δ⊢env 2 ...

    work page 2025

  56. [56]

    We must now show that R indeed is a typing interpretation according to Definition 3.8

    ∈ R Σ,Γ,env𝑇 ∧𝑠 ′ 1 ⊒𝑠 ′ 2 ⊒fst(𝑄 ′) and clearly, since(𝑄,Δ, 𝑠 1) ∈ R Σ,Γ,env𝑇 and𝑠 1 ⊒𝑠 2 ⊒fst(𝑄), we also have that(𝑄,Δ, 𝑠 2) ∈ R. We must now show that R indeed is a typing interpretation according to Definition 3.8. Pick any (𝑄 ′,Δ ′, 𝑠′

    work page

  57. [57]

    (2) Otherwise, we know that (𝑄 ′,Δ ′, 𝑠′

    ∈ R; there are now two cases: (1) If𝑄 ′ ∈ T Q, then it satisfies Case 1 of Definition 3.8. (2) Otherwise, we know that (𝑄 ′,Δ ′, 𝑠′

    work page

  58. [58]

    ∈ R Σ,Γ,env𝑇 and, for all appropriately shaped env𝑆𝑉 , there exists at least one transition Σ;Γ;Δ ′ ⊨𝑠 ′ 1 ⟨𝑄 ′,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ ′′ ⊨𝑠 ′′ 1 𝑄 ′′,env 𝑇 ;env ′ 𝑆𝑉 such that(𝑄 ′′,Δ ′′, 𝑠′′ 1 ) ∈ R Σ,Γ,env𝑇 . By Proposition 3.1, we then have that the transition Σ;Γ;Δ ′ ⊨𝑠 ′ 2 ⟨𝑄 ′,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ ′′ ⊨𝑠 ′′ 2 𝑄 ′′,env 𝑇 ;env ′ 𝑆𝑉 can be concluded for any 𝑠 ′...

    work page 2025

  59. [59]

    ∈ R 1 Σ,Γ,env𝑇 . Therefore, the transition Σ;Γ;Δ 1 ⊨𝑠1 ⟨𝑞1;𝑄,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ ′ 1 ⊨𝑠 ′ 1 𝑞′ 1;𝑄,env 𝑇 ;env ′ 𝑆𝑉 can be concluded by the same rule, and by construction of R, we have that (𝑞′ 1; 𝑄,Δ ′ 1, 𝑠′

    work page

  60. [60]

    • A special case of the above is if 𝑞′ 1 in the reduct is empty

    ∈ R . • A special case of the above is if 𝑞′ 1 in the reduct is empty. Again we have that (𝑞1; ⊥,Δ 1, 𝑠1) ∈ R1 Σ,Γ,env𝑇 by construction ofR, and we know the transition Σ;Γ;Δ 1 ⊨𝑠1 ⟨𝑞1;⊥,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ ′ 1 ⊨𝑠 ′ 1 ⊥,env 𝑇 ;env ′ 𝑆𝑉 can be concluded by some rule, and(⊥,Δ ′ 1, 𝑠′

    work page

  61. [61]

    Still by construction ofR, we know that fin(𝑞1; ⊥,Δ 1, 𝑠1)=(Δ, 𝑠) and, since the execution terminates, we have by Theorem H.3 thatΔ ′ 1 =Δand𝑠 ′ 1 =𝑠

    ∈ R 1 Σ,Γ,env𝑇 . Still by construction ofR, we know that fin(𝑞1; ⊥,Δ 1, 𝑠1)=(Δ, 𝑠) and, since the execution terminates, we have by Theorem H.3 thatΔ ′ 1 =Δand𝑠 ′ 1 =𝑠. By the same reasoning as above, the transition Σ;Γ;Δ 1 ⊨𝑠1 ⟨𝑞1;𝑄,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ⊨ 𝑠 𝑄,env 𝑇 ;env ′ 𝑆𝑉 can therefore be concluded and, since (𝑄,Δ, 𝑠) ∈ R 2 Σ,Γ,env𝑇 , we also have that (𝑄,...

    work page

  62. [62]

    Therefore we also have that (𝑄 ′ 1,Δ ′ 1, 𝑠′

    ∈ R 2 Σ,Γ,env𝑇 . Therefore we also have that (𝑄 ′ 1,Δ ′ 1, 𝑠′

    work page

  63. [63]

    ∈ R by construction.□ Notice that, in the construction of the candidate typing interpretation R of the previous proof, we make use of two related facts: • Transitions only ever modifythe topof the stack; hence, we can remove the ⊥ symbol from a stack𝑞;⊥and suffix another stack𝑄onto it. • Theorem H.3 tells us that,if 𝑞; ⊥ eventually terminates normally whe...

    work page 2025

  64. [64]

    There are now two possi- bilities, depending on the shape of𝑞 ′ 1: –If𝑞 ′ 1 is empty, the reduct is of the formΣ;Γ;Δ⊨ 𝑠 ⊥,env 𝑇 ;env ′ 𝑆𝑉

    ∈ R 1 Σ,Γ,env𝑇 . There are now two possi- bilities, depending on the shape of𝑞 ′ 1: –If𝑞 ′ 1 is empty, the reduct is of the formΣ;Γ;Δ⊨ 𝑠 ⊥,env 𝑇 ;env ′ 𝑆𝑉 . Then, the transition Σ;Γ;Δ 1 ⊨𝑠1 ⟨𝑞1;𝑠;⊥,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ⊨ 𝑠 𝑠;⊥,env 𝑇 ;env ′ 𝑆𝑉 can likewise be concluded, and(𝑠;⊥,Δ, 𝑠) ∈ Rby construction. – Otherwise, if 𝑞′ 1 is non-empty, then the reduct is ins...

    work page

  65. [65]

    Then, the transition Σ;Γ;Δ 1 ⊨𝑠1 ⟨𝑞1;𝑠;⊥,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ ′ 1 ⊨𝑠 ′ 1 𝑞′ 1;𝑠;⊥,env 𝑇 ;env ′ 𝑆𝑉 can likewise be concluded

    ∈ R 1 Σ,Γ,env𝑇 . Then, the transition Σ;Γ;Δ 1 ⊨𝑠1 ⟨𝑞1;𝑠;⊥,env 𝑇 𝑆𝑉 ⟩ →Σ;Γ;Δ ′ 1 ⊨𝑠 ′ 1 𝑞′ 1;𝑠;⊥,env 𝑇 ;env ′ 𝑆𝑉 can likewise be concluded. Finally, by Theorem H.3, we have thatfin(𝑞 ′ 1; ⊥,Δ ′ 1, 𝑠′ 1)=(Δ, 𝑠) , so by construction we also have that(𝑞 ′ 1;𝑠;⊥,Δ ′ 1, 𝑠′

    work page

  66. [66]

    By the definition of Σ; Γ; Δ; env𝑇 ⊨while𝑒do𝑆 : cmd(𝑠) , we must exhibit a typing interpretationR ′ Σ,Γ,env𝑇 containing the triplet(while𝑒do𝑆;⊥,Δ, 𝑠)

    ∈ R.□ Proof of Lemma 3.21. By the definition of Σ; Γ; Δ; env𝑇 ⊨while𝑒do𝑆 : cmd(𝑠) , we must exhibit a typing interpretationR ′ Σ,Γ,env𝑇 containing the triplet(while𝑒do𝑆;⊥,Δ, 𝑠). From Σ; Γ; Δ; env𝑇 ⊨𝑆 : cmd(𝑠) we know that there exists a typing interpretation RΣ,Γ,env𝑇 such that (𝑆,Δ, 𝑠) ∈ R Σ,Γ,env𝑇 . We then construct the following candidate typing inter...

    work page 2025